0.009/0.009 YES 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Inlining of Conditions Processor [STERN17]: 0.009/0.009 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Critical Pairs Processor: 0.009/0.009 -> Rules: 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 -> Vars: 0.009/0.009 0.009/0.009 -> FVars: 0.009/0.009 0.009/0.009 -> PVars: 0.009/0.009 0.009/0.009 0.009/0.009 -> Rlps: 0.009/0.009 crule: a -> c | b ->* c, id: 1, possubterms: a-> [] 0.009/0.009 crule: b -> c, id: 2, possubterms: b-> [] 0.009/0.009 crule: f(b) -> f(a), id: 3, possubterms: f(b)-> [], b-> [1] 0.009/0.009 0.009/0.009 -> Unifications: 0.009/0.009 R3 unifies with R2 at p: [1], l: f(b), lp: b, conds: {}, sig: {}, l': b, r: f(a), r': c 0.009/0.009 0.009/0.009 -> Critical pairs info: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Maybe terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 Underlying TRS Termination Processor: 0.009/0.009 0.009/0.009 Resulting Underlying TRS: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Underlying TRS terminating? 0.009/0.009 YES 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 (VAR vu95NonEmpty:S vNonEmptyu58S:S) 0.009/0.009 (RULES 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Dependency Pairs Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> A 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 SCC Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> A 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ->Strongly Connected Components: 0.009/0.009 ->->Cycle: 0.009/0.009 ->->-> Pairs: 0.009/0.009 F(b) -> F(a) 0.009/0.009 ->->-> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Reduction Pair Processor: 0.009/0.009 -> Pairs: 0.009/0.009 F(b) -> F(a) 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 -> Usable rules: 0.009/0.009 a -> c 0.009/0.009 ->Interpretation type: 0.009/0.009 Linear 0.009/0.009 ->Coefficients: 0.009/0.009 Natural Numbers 0.009/0.009 ->Dimension: 0.009/0.009 1 0.009/0.009 ->Bound: 0.009/0.009 2 0.009/0.009 ->Interpretation: 0.009/0.009 0.009/0.009 [a] = 1 0.009/0.009 [b] = 2 0.009/0.009 [f](X) = 0 0.009/0.009 [c] = 1 0.009/0.009 [fSNonEmpty] = 0 0.009/0.009 [A] = 0 0.009/0.009 [F](X) = 2.X 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 SCC Processor: 0.009/0.009 -> Pairs: 0.009/0.009 Empty 0.009/0.009 -> Rules: 0.009/0.009 a -> c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ->Strongly Connected Components: 0.009/0.009 There is no strongly connected component 0.009/0.009 0.009/0.009 The problem is finite. 0.009/0.009 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:YES 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Maybe right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Maybe almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Right Stable Processor: 0.009/0.009 Right-stable CTRS 0.009/0.009 Justification: 0.009/0.009 0.009/0.009 -> Term right-stability conditions: 0.009/0.009 Term: c 0.009/0.009 Right-stable term 0.009/0.009 Linear constructor form 0.009/0.009 Don't know if term is a ground normal form (not needed) 0.009/0.009 Right-stability condition achieved 0.009/0.009 A call to InfChecker wasn't needed 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:YES 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Right-stable CTRS, Not overlay CTRS 0.009/0.009 Maybe normal CTRS, Almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Normal RConds Processor: 0.009/0.009 YES 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Infeasibility Problem: 0.009/0.009 [(VAR vNonEmpty:S x1:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 )] 0.009/0.009 0.009/0.009 Infeasibility Conditions: 0.009/0.009 c -> x1:S 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 0.009/0.009 Obtaining a model using Mace4: 0.009/0.009 0.009/0.009 -> Usable Rules: 0.009/0.009 Empty 0.009/0.009 0.009/0.009 -> Mace4 Output: 0.009/0.009 ============================== Mace4 ================================= 0.009/0.009 Mace4 (64) version 2009-11A, November 2009. 0.009/0.009 Process 59934 was started by ubuntu on ubuntu, 0.009/0.009 Wed Jul 14 11:32:12 2021 0.009/0.009 The command was "./mace4 -c -f /tmp/mace459921-2.in". 0.009/0.009 ============================== end of head =========================== 0.009/0.009 0.009/0.009 ============================== INPUT ================================= 0.009/0.009 0.009/0.009 % Reading from file /tmp/mace459921-2.in 0.009/0.009 0.009/0.009 assign(max_seconds,1). 0.009/0.009 0.009/0.009 formulas(assumptions). 0.009/0.009 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(goals). 0.009/0.009 (exists x1 ->(c,x1)) # label(goal). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 ============================== end of input ========================== 0.009/0.009 0.009/0.009 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.009/0.009 0.009/0.009 % Formulas that are not ordinary clauses: 0.009/0.009 1 ->(x1,y) -> ->(f(x1),f(y)) # label(congruence) # label(non_clause). [assumption]. 0.009/0.009 2 (exists x1 ->(c,x1)) # label(goal) # label(non_clause) # label(goal). [goal]. 0.009/0.009 0.009/0.009 ============================== end of process non-clausal formulas === 0.009/0.009 0.009/0.009 ============================== CLAUSES FOR SEARCH ==================== 0.009/0.009 0.009/0.009 formulas(mace4_clauses). 0.009/0.009 -->(x,y) | ->(f(x),f(y)) # label(congruence). 0.009/0.009 -->(c,x) # label(goal). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 ============================== end of clauses for search ============= 0.009/0.009 0.009/0.009 % There are no natural numbers in the input. 0.009/0.009 0.009/0.009 ============================== DOMAIN SIZE 2 ========================= 0.009/0.009 0.009/0.009 ============================== MODEL ================================= 0.009/0.009 0.009/0.009 interpretation( 2, [number=1, seconds=0], [ 0.009/0.009 0.009/0.009 function(c, [ 0 ]), 0.009/0.009 0.009/0.009 function(f(_), [ 0, 0 ]), 0.009/0.009 0.009/0.009 relation(->(_,_), [ 0.009/0.009 0, 0, 0.009/0.009 0, 0 ]) 0.009/0.009 ]). 0.009/0.009 0.009/0.009 ============================== end of model ========================== 0.009/0.009 0.009/0.009 ============================== STATISTICS ============================ 0.009/0.009 0.009/0.009 For domain size 2. 0.009/0.009 0.009/0.009 Current CPU time: 0.00 seconds (total CPU time: 0.00 seconds). 0.009/0.009 Ground clauses: seen=6, kept=6. 0.009/0.009 Selections=3, assignments=3, propagations=4, current_models=1. 0.009/0.009 Rewrite_terms=10, rewrite_bools=8, indexes=2. 0.009/0.009 Rules_from_neg_clauses=0, cross_offs=0. 0.009/0.009 0.009/0.009 ============================== end of statistics ===================== 0.009/0.009 0.009/0.009 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.009/0.009 0.009/0.009 Exiting with 1 model. 0.009/0.009 0.009/0.009 Process 59934 exit (max_models) Wed Jul 14 11:32:12 2021 0.009/0.009 The process finished Wed Jul 14 11:32:12 2021 0.009/0.009 0.009/0.009 0.009/0.009 Mace4 cooked interpretation: 0.009/0.009 0.009/0.009 0.009/0.009 0.009/0.009 The problem is infeasible. 0.009/0.009 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Right-stable CTRS, Not overlay CTRS 0.009/0.009 Normal CTRS, Almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 0.009/0.009 Problem 1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:YES 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Right-stable CTRS, Not overlay CTRS 0.009/0.009 Normal CTRS, Almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Conditional Critical Pairs Distributor Processor 0.009/0.009 Problem 1.1: 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 Confluence Problem: 0.009/0.009 (VAR vNonEmpty:S) 0.009/0.009 (STRATEGY CONTEXTSENSITIVE 0.009/0.009 (a) 0.009/0.009 (b) 0.009/0.009 (f 1) 0.009/0.009 (c) 0.009/0.009 (fSNonEmpty) 0.009/0.009 ) 0.009/0.009 (RULES 0.009/0.009 a -> c | b ->* c 0.009/0.009 b -> c 0.009/0.009 f(b) -> f(a) 0.009/0.009 ) 0.009/0.009 Critical Pairs: 0.009/0.009 => Not trivial, Not overlay, N1 0.009/0.009 Terminating:YES 0.009/0.009 0.009/0.009 -> Problem conclusions: 0.009/0.009 Left linear, Right linear, Linear 0.009/0.009 Not weakly orthogonal, Not almost orthogonal, Not orthogonal 0.009/0.009 CTRS Type: 1 0.009/0.009 Deterministic, Strongly deterministic 0.009/0.009 Oriented CTRS, Properly oriented CTRS, Not join CTRS 0.009/0.009 Right-stable CTRS, Not overlay CTRS 0.009/0.009 Normal CTRS, Almost normal CTRS 0.009/0.009 Terminating CTRS, Maybe joinable CCPs 0.009/0.009 Maybe level confluent 0.009/0.009 Maybe confluent 0.009/0.009 ::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: 0.009/0.009 0.009/0.009 Prover9 CCP Convergence Checker Processor: 0.009/0.009 formulas(sos). 0.009/0.009 %Reflexivity 0.009/0.009 reds(x,x). 0.009/0.009 0.009/0.009 %Transitivity 0.009/0.009 (red(x,y) & reds(y,z)) -> reds(x,z). 0.009/0.009 0.009/0.009 %Congruence 0.009/0.009 0.009/0.009 0.009/0.009 red(x,y) -> red(f(x),f(y)). 0.009/0.009 0.009/0.009 %Replacement 0.009/0.009 reds(b,c) -> red(a,c). 0.009/0.009 red(b,c). 0.009/0.009 red(f(b),f(a)). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(goals). 0.009/0.009 exists z (reds(f(c),z) & reds(f(a),z)). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 Proof: 0.009/0.009 ============================== Prover9 =============================== 0.009/0.009 Prover9 (64) version 2009-11A, November 2009. 0.009/0.009 Process 59947 was started by ubuntu on ubuntu, 0.009/0.009 Wed Jul 14 11:32:12 2021 0.009/0.009 The command was "./prover9 -t 5 -f /tmp/prover959897-4.in". 0.009/0.009 ============================== end of head =========================== 0.009/0.009 0.009/0.009 ============================== INPUT ================================= 0.009/0.009 0.009/0.009 % Reading from file /tmp/prover959897-4.in 0.009/0.009 0.009/0.009 0.009/0.009 formulas(sos). 0.009/0.009 reds(x,x). 0.009/0.009 red(x,y) & reds(y,z) -> reds(x,z). 0.009/0.009 red(x,y) -> red(f(x),f(y)). 0.009/0.009 reds(b,c) -> red(a,c). 0.009/0.009 red(b,c). 0.009/0.009 red(f(b),f(a)). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(goals). 0.009/0.009 (exists z (reds(f(c),z) & reds(f(a),z))). 0.009/0.009 end_of_list. 0.009/0.009 assign(max_megs,-1). 0.009/0.009 set(quiet). 0.009/0.009 0.009/0.009 ============================== end of input ========================== 0.009/0.009 0.009/0.009 % From the command line: assign(max_seconds, 5). 0.009/0.009 0.009/0.009 ============================== PROCESS NON-CLAUSAL FORMULAS ========== 0.009/0.009 0.009/0.009 % Formulas that are not ordinary clauses: 0.009/0.009 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.009/0.009 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 0.009/0.009 3 reds(b,c) -> red(a,c) # label(non_clause). [assumption]. 0.009/0.009 4 (exists z (reds(f(c),z) & reds(f(a),z))) # label(non_clause) # label(goal). [goal]. 0.009/0.009 0.009/0.009 ============================== end of process non-clausal formulas === 0.009/0.009 0.009/0.009 ============================== PROCESS INITIAL CLAUSES =============== 0.009/0.009 0.009/0.009 % Clauses before input processing: 0.009/0.009 0.009/0.009 formulas(usable). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(sos). 0.009/0.009 reds(x,x). [assumption]. 0.009/0.009 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.009/0.009 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 0.009/0.009 -reds(b,c) | red(a,c). [clausify(3)]. 0.009/0.009 red(b,c). [assumption]. 0.009/0.009 red(f(b),f(a)). [assumption]. 0.009/0.009 -reds(f(c),x) | -reds(f(a),x). [deny(4)]. 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(demodulators). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 ============================== PREDICATE ELIMINATION ================= 0.009/0.009 0.009/0.009 ============================== end predicate elimination ============= 0.009/0.009 0.009/0.009 Auto_denials: (no changes). 0.009/0.009 0.009/0.009 Term ordering decisions: 0.009/0.009 0.009/0.009 kept: 5 reds(x,x). [assumption]. 0.009/0.009 kept: 6 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.009/0.009 kept: 7 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 0.009/0.009 kept: 8 -reds(b,c) | red(a,c). [clausify(3)]. 0.009/0.009 kept: 9 red(b,c). [assumption]. 0.009/0.009 kept: 10 red(f(b),f(a)). [assumption]. 0.009/0.009 kept: 11 -reds(f(c),x) | -reds(f(a),x). [deny(4)]. 0.009/0.009 0.009/0.009 ============================== end of process initial clauses ======== 0.009/0.009 0.009/0.009 ============================== CLAUSES FOR SEARCH ==================== 0.009/0.009 0.009/0.009 % Clauses after input processing: 0.009/0.009 0.009/0.009 formulas(usable). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(sos). 0.009/0.009 5 reds(x,x). [assumption]. 0.009/0.009 6 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.009/0.009 7 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 0.009/0.009 8 -reds(b,c) | red(a,c). [clausify(3)]. 0.009/0.009 9 red(b,c). [assumption]. 0.009/0.009 10 red(f(b),f(a)). [assumption]. 0.009/0.009 11 -reds(f(c),x) | -reds(f(a),x). [deny(4)]. 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 formulas(demodulators). 0.009/0.009 end_of_list. 0.009/0.009 0.009/0.009 ============================== end of clauses for search ============= 0.009/0.009 0.009/0.009 ============================== SEARCH ================================ 0.009/0.009 0.009/0.009 % Starting search at 0.00 seconds. 0.009/0.009 0.009/0.009 given #1 (I,wt=3): 5 reds(x,x). [assumption]. 0.009/0.009 0.009/0.009 given #2 (I,wt=9): 6 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.009/0.009 0.009/0.009 given #3 (I,wt=8): 7 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 0.009/0.009 0.009/0.009 given #4 (I,wt=6): 8 -reds(b,c) | red(a,c). [clausify(3)]. 0.009/0.009 0.009/0.009 given #5 (I,wt=3): 9 red(b,c). [assumption]. 0.009/0.009 0.009/0.009 given #6 (I,wt=5): 10 red(f(b),f(a)). [assumption]. 0.009/0.009 0.009/0.009 given #7 (I,wt=8): 11 -reds(f(c),x) | -reds(f(a),x). [deny(4)]. 0.009/0.009 0.009/0.009 given #8 (A,wt=5): 12 red(f(b),f(c)). [ur(7,a,9,a)]. 0.009/0.009 0.009/0.009 given #9 (F,wt=5): 18 -reds(f(a),f(c)). [resolve(11,a,5,a)]. 0.009/0.009 0.009/0.009 given #10 (F,wt=5): 20 -reds(f(c),f(a)). [resolve(11,b,5,a)]. 0.009/0.009 0.009/0.009 given #11 (F,wt=5): 24 -red(f(a),f(c)). [ur(6,b,5,a,c,18,a)]. 0.009/0.009 0.009/0.009 ============================== PROOF ================================= 0.009/0.009 0.009/0.009 % Proof 1 at 0.00 (+ 0.00) seconds. 0.009/0.009 % Length of proof is 15. 0.009/0.009 % Level of proof is 4. 0.009/0.009 % Maximum clause weight is 9.000. 0.009/0.009 % Given clauses 11. 0.009/0.009 0.009/0.009 1 red(x,y) & reds(y,z) -> reds(x,z) # label(non_clause). [assumption]. 0.009/0.009 2 red(x,y) -> red(f(x),f(y)) # label(non_clause). [assumption]. 0.009/0.009 3 reds(b,c) -> red(a,c) # label(non_clause). [assumption]. 0.009/0.009 4 (exists z (reds(f(c),z) & reds(f(a),z))) # label(non_clause) # label(goal). [goal]. 0.009/0.009 5 reds(x,x). [assumption]. 0.009/0.009 6 -red(x,y) | -reds(y,z) | reds(x,z). [clausify(1)]. 0.009/0.009 7 -red(x,y) | red(f(x),f(y)). [clausify(2)]. 0.009/0.009 8 -reds(b,c) | red(a,c). [clausify(3)]. 0.009/0.009 9 red(b,c). [assumption]. 0.009/0.009 11 -reds(f(c),x) | -reds(f(a),x). [deny(4)]. 0.009/0.009 13 reds(b,c). [ur(6,a,9,a,b,5,a)]. 0.009/0.009 14 red(a,c). [back_unit_del(8),unit_del(a,13)]. 0.009/0.009 18 -reds(f(a),f(c)). [resolve(11,a,5,a)]. 0.009/0.009 24 -red(f(a),f(c)). [ur(6,b,5,a,c,18,a)]. 0.009/0.009 27 $F. [resolve(24,a,7,b),unit_del(a,14)]. 0.009/0.009 0.009/0.009 ============================== end of proof ========================== 0.009/0.009 0.009/0.009 ============================== STATISTICS ============================ 0.009/0.009 0.009/0.009 Given=11. Generated=25. Kept=22. proofs=1. 0.009/0.009 Usable=10. Sos=11. Demods=0. Limbo=0, Disabled=8. Hints=0. 0.009/0.009 Kept_by_rule=0, Deleted_by_rule=0. 0.009/0.009 Forward_subsumed=2. Back_subsumed=0. 0.009/0.009 Sos_limit_deleted=0. Sos_displaced=0. Sos_removed=0. 0.009/0.009 New_demodulators=0 (0 lex), Back_demodulated=0. Back_unit_deleted=1. 0.009/0.009 Demod_attempts=0. Demod_rewrites=0. 0.009/0.009 Res_instance_prunes=0. Para_instance_prunes=0. Basic_paramod_prunes=0. 0.009/0.009 Nonunit_fsub_feature_tests=4. Nonunit_bsub_feature_tests=29. 0.009/0.009 Megabytes=0.06. 0.009/0.009 User_CPU=0.00, System_CPU=0.00, Wall_clock=0. 0.009/0.009 0.009/0.009 ============================== end of statistics ===================== 0.009/0.009 0.009/0.009 ============================== end of search ========================= 0.009/0.009 0.009/0.009 THEOREM PROVED 0.009/0.009 0.009/0.009 Exiting with 1 proof. 0.009/0.009 0.009/0.009 Process 59947 exit (max_proofs) Wed Jul 14 11:32:12 2021 0.009/0.009 0.009/0.009 0.009/0.009 The problem is joinable. 0.009/0.009 0.07user 0.02system 0:00.09elapsed 100%CPU (0avgtext+0avgdata 14912maxresident)k 0.009/0.009 8inputs+0outputs (0major+6946minor)pagefaults 0swaps