25.038/25.038 YES 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR vNonEmpty:S x:S y:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 tc(x:S) -> y:S | pin(x:S) ->* pout(z), tc(z) ->* y:S 25.038/25.038 ) 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Inlining of Conditions Processor [STERN17]: 25.038/25.038 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR vNonEmpty:S x:S y:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> tc(z) | pin(x:S) ->* pout(z) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Clean CTRS Processor: 25.038/25.038 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 CRule InfChecker Info: 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 Rule remains 25.038/25.038 Proof: 25.038/25.038 NO_CONDS 25.038/25.038 25.038/25.038 CRule InfChecker Info: 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 Rule remains 25.038/25.038 Proof: 25.038/25.038 NO_CONDS 25.038/25.038 25.038/25.038 CRule InfChecker Info: 25.038/25.038 tc(x:S) -> tc(z) | pin(x:S) ->* pout(z) 25.038/25.038 Rule deleted 25.038/25.038 Proof: 25.038/25.038 YES 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Infeasibility Problem: 25.038/25.038 [(VAR vNonEmpty:S vNonEmpty:S:S x:S:S y:S:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S:S) -> tc(z) | pin(x:S:S) ->* pout(z) 25.038/25.038 tc(x:S:S) -> x:S:S 25.038/25.038 )] 25.038/25.038 25.038/25.038 Infeasibility Conditions: 25.038/25.038 pin(x:S:S) ->* pout(z) 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Obtaining a model using Mace4: 25.038/25.038 25.038/25.038 -> Usable Rules: 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S:S) -> tc(z) | pin(x:S:S) ->* pout(z) 25.038/25.038 tc(x:S:S) -> x:S:S 25.038/25.038 25.038/25.038 -> Mace4 Output: 25.038/25.038 ============================== Mace4 ================================= 25.038/25.038 Mace4 (64) version 2009-11A, November 2009. 25.038/25.038 Process 100486 was started by ubuntu on ubuntu, 25.038/25.038 Fri Jul 16 14:36:51 2021 25.038/25.038 The command was "./mace4 -c -f /tmp/mace4100473-2.in". 25.038/25.038 ============================== end of head =========================== 25.038/25.038 25.038/25.038 ============================== INPUT ================================= 25.038/25.038 25.038/25.038 % Reading from file /tmp/mace4100473-2.in 25.038/25.038 25.038/25.038 assign(max_seconds,10). 25.038/25.038 25.038/25.038 formulas(assumptions). 25.038/25.038 ->(x1,y) -> ->(pin(x1),pin(y)) # label(congruence). 25.038/25.038 ->(x1,y) -> ->(tc(x1),tc(y)) # label(congruence). 25.038/25.038 ->(x1,y) -> ->(pout(x1),pout(y)) # label(congruence). 25.038/25.038 ->(pin(a),pout(b)) # label(replacement). 25.038/25.038 ->(pin(b),pout(c)) # label(replacement). 25.038/25.038 ->*(pin(x2),pout(z)) -> ->(tc(x2),tc(z)) # label(replacement). 25.038/25.038 ->(tc(x2),x2) # label(replacement). 25.038/25.038 ->*(x,x) # label(reflexivity). 25.038/25.038 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity). 25.038/25.038 end_of_list. 25.038/25.038 25.038/25.038 formulas(goals). 25.038/25.038 (exists x2 ->*(pin(x2),pout(z))) # label(goal). 25.038/25.038 end_of_list. 25.038/25.038 25.038/25.038 ============================== end of input ========================== 25.038/25.038 25.038/25.038 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 25.038/25.038 25.038/25.038 % Formulas that are not ordinary clauses: 25.038/25.038 1 ->(x1,y) -> ->(pin(x1),pin(y)) # label(congruence) # label(non_clause). [assumption]. 25.038/25.038 2 ->(x1,y) -> ->(tc(x1),tc(y)) # label(congruence) # label(non_clause). [assumption]. 25.038/25.038 3 ->(x1,y) -> ->(pout(x1),pout(y)) # label(congruence) # label(non_clause). [assumption]. 25.038/25.038 4 ->*(pin(x2),pout(z)) -> ->(tc(x2),tc(z)) # label(replacement) # label(non_clause). [assumption]. 25.038/25.038 5 ->(x,y) & ->*(y,z) -> ->*(x,z) # label(transitivity) # label(non_clause). [assumption]. 25.038/25.038 6 (exists x2 ->*(pin(x2),pout(z))) # label(goal) # label(non_clause) # label(goal). [goal]. 25.038/25.038 25.038/25.038 ============================== end of process non-clausal formulas === 25.038/25.038 25.038/25.038 ============================== CLAUSES FOR SEARCH ==================== 25.038/25.038 25.038/25.038 formulas(mace4_clauses). 25.038/25.038 -->(x,y) | ->(pin(x),pin(y)) # label(congruence). 25.038/25.038 -->(x,y) | ->(tc(x),tc(y)) # label(congruence). 25.038/25.038 -->(x,y) | ->(pout(x),pout(y)) # label(congruence). 25.038/25.038 ->(pin(a),pout(b)) # label(replacement). 25.038/25.038 ->(pin(b),pout(c)) # label(replacement). 25.038/25.038 -->*(pin(x),pout(z)) | ->(tc(x),tc(z)) # label(replacement). 25.038/25.038 ->(tc(x),x) # label(replacement). 25.038/25.038 ->*(x,x) # label(reflexivity). 25.038/25.038 -->(x,y) | -->*(y,z) | ->*(x,z) # label(transitivity). 25.038/25.038 -->*(pin(x),pout(z)) # label(goal). 25.038/25.038 end_of_list. 25.038/25.038 25.038/25.038 ============================== end of clauses for search ============= 25.038/25.038 25.038/25.038 % There are no natural numbers in the input. 25.038/25.038 25.038/25.038 ============================== DOMAIN SIZE 2 ========================= 25.038/25.038 25.038/25.038 ============================== MODEL ================================= 25.038/25.038 25.038/25.038 interpretation( 2, [number=1, seconds=0], [ 25.038/25.038 25.038/25.038 function(a, [ 0 ]), 25.038/25.038 25.038/25.038 function(b, [ 0 ]), 25.038/25.038 25.038/25.038 function(c, [ 0 ]), 25.038/25.038 25.038/25.038 function(z, [ 1 ]), 25.038/25.038 25.038/25.038 function(pin(_), [ 0, 0 ]), 25.038/25.038 25.038/25.038 function(tc(_), [ 0, 1 ]), 25.038/25.038 25.038/25.038 function(pout(_), [ 0, 1 ]), 25.038/25.038 25.038/25.038 relation(->*(_,_), [ 25.038/25.038 1, 0, 25.038/25.038 0, 1 ]), 25.038/25.038 25.038/25.038 relation(->(_,_), [ 25.038/25.038 1, 0, 25.038/25.038 0, 1 ]) 25.038/25.038 ]). 25.038/25.038 25.038/25.038 ============================== end of model ========================== 25.038/25.038 25.038/25.038 ============================== STATISTICS ============================ 25.038/25.038 25.038/25.038 For domain size 2. 25.038/25.038 25.038/25.038 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 25.038/25.038 Ground clauses: seen=30, kept=26. 25.038/25.038 Selections=8, assignments=10, propagations=17, current_models=1. 25.038/25.038 Rewrite_terms=94, rewrite_bools=40, indexes=37. 25.038/25.038 Rules_from_neg_clauses=6, cross_offs=6. 25.038/25.038 25.038/25.038 ============================== end of statistics ===================== 25.038/25.038 25.038/25.038 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 25.038/25.038 25.038/25.038 Exiting with 1 model. 25.038/25.038 25.038/25.038 Process 100486 exit (max_models) Fri Jul 16 14:36:51 2021 25.038/25.038 The process finished Fri Jul 16 14:36:51 2021 25.038/25.038 25.038/25.038 25.038/25.038 Mace4 cooked interpretation: 25.038/25.038 25.038/25.038 25.038/25.038 25.038/25.038 The problem is infeasible. 25.038/25.038 25.038/25.038 25.038/25.038 CRule InfChecker Info: 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 Rule remains 25.038/25.038 Proof: 25.038/25.038 NO_CONDS 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Transform No Conds CTRS Processor: 25.038/25.038 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Resulting R: 25.038/25.038 (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 CleanTRS Processor: 25.038/25.038 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (tc 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (fSNonEmpty) 25.038/25.038 (pout 1) 25.038/25.038 (z) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 25.038/25.038 Problem 1: 25.038/25.038 25.038/25.038 Modular Confluence Combinations Decomposition Processor: 25.038/25.038 25.038/25.038 TRS combination: 25.038/25.038 {pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c)} 25.038/25.038 {tc(x:S) -> x:S} 25.038/25.038 Disjoint 25.038/25.038 Constructor-sharing 25.038/25.038 Left linear 25.038/25.038 Not layer-preserving 25.038/25.038 TRS1 25.038/25.038 Just (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (pout 1) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 ) 25.038/25.038 25.038/25.038 TRS2 25.038/25.038 Just (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (tc 1) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 25.038/25.038 25.038/25.038 The problem is decomposed in 2 subproblems. 25.038/25.038 25.038/25.038 Problem 1.1: 25.038/25.038 Linearity Processor: 25.038/25.038 Linear? 25.038/25.038 YES 25.038/25.038 Problem 1.1.1: 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (pin 1) 25.038/25.038 (a) 25.038/25.038 (b) 25.038/25.038 (c) 25.038/25.038 (pout 1) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 ) 25.038/25.038 Linear:YES 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 Huet Levy Processor: 25.038/25.038 -> Rules: 25.038/25.038 pin(a) -> pout(b) 25.038/25.038 pin(b) -> pout(c) 25.038/25.038 -> Vars: 25.038/25.038 25.038/25.038 -> FVars: 25.038/25.038 25.038/25.038 -> PVars: 25.038/25.038 25.038/25.038 25.038/25.038 -> Rlps: 25.038/25.038 (rule: pin(a) -> pout(b), id: 1, possubterms: pin(a)->[], a->[1]) 25.038/25.038 (rule: pin(b) -> pout(c), id: 2, possubterms: pin(b)->[], b->[1]) 25.038/25.038 25.038/25.038 -> Unifications: 25.038/25.038 25.038/25.038 25.038/25.038 -> Critical pairs info: 25.038/25.038 25.038/25.038 25.038/25.038 -> Problem conclusions: 25.038/25.038 Left linear, Right linear, Linear 25.038/25.038 Weakly orthogonal, Almost orthogonal, Orthogonal 25.038/25.038 Huet-Levy confluent, Not Newman confluent 25.038/25.038 R is a TRS 25.038/25.038 25.038/25.038 25.038/25.038 The problem is joinable. 25.038/25.038 25.038/25.038 Problem 1.2: 25.038/25.038 Linearity Processor: 25.038/25.038 Linear? 25.038/25.038 YES 25.038/25.038 Problem 1.2.1: 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 Confluence Problem: 25.038/25.038 (VAR x:S) 25.038/25.038 (STRATEGY CONTEXTSENSITIVE 25.038/25.038 (tc 1) 25.038/25.038 ) 25.038/25.038 (RULES 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 ) 25.038/25.038 Linear:YES 25.038/25.038 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 25.038/25.038 25.038/25.038 Huet Levy Processor: 25.038/25.038 -> Rules: 25.038/25.038 tc(x:S) -> x:S 25.038/25.038 -> Vars: 25.038/25.038 x 25.038/25.038 -> FVars: 25.038/25.038 x2 25.038/25.038 -> PVars: 25.038/25.038 x: [x2] 25.038/25.038 25.038/25.038 -> Rlps: 25.038/25.038 (rule: tc(x2:S) -> x2:S, id: 1, possubterms: tc(x2:S)->[]) 25.038/25.038 25.038/25.038 -> Unifications: 25.038/25.038 25.038/25.038 25.038/25.038 -> Critical pairs info: 25.038/25.038 25.038/25.038 25.038/25.038 -> Problem conclusions: 25.038/25.038 Left linear, Right linear, Linear 25.038/25.038 Weakly orthogonal, Almost orthogonal, Orthogonal 25.038/25.038 Huet-Levy confluent, Not Newman confluent 25.038/25.038 R is a TRS 25.038/25.038 25.038/25.038 25.038/25.038 The problem is joinable. 25.038/25.038 22.93user 0.76system 0:25.38elapsed 93%CPU (0avgtext+0avgdata 135928maxresident)k 25.038/25.038 8inputs+0outputs (0major+74886minor)pagefaults 0swaps