%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LDA002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:00:18 AM UTC 2026
% Result : Unsatisfiable 0.75s 0.52s
% Output : CNFRefutation 0.75s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 12
% Syntax : Number of formulae : 109 ( 109 unt; 0 def)
% Number of atoms : 109 ( 108 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-2 aty)
% Number of variables : 25 ( 0 sgn 3 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(a1,axiom,
! [VAR_0,VAR_1,VAR_2] : f(VAR_0,f(VAR_1,VAR_2)) = f(f(VAR_0,VAR_1),f(VAR_0,VAR_2)),
file('theBenchmark.p',a1) ).
cnf(c_1,plain,
f(A,f(B,C)) = f(f(A,B),f(A,C)),
inference(clausify,[status(thm)],[a1]) ).
cnf(c_2,plain,
f(f(A,B),f(A,C)) = f(A,f(B,C)),
inference(copy,[status(thm)],[c_1]) ).
fof(clause_2,axiom,
n2 = f(n1,n1),
file('theBenchmark.p',clause_2) ).
cnf(c_3,plain,
n2 = f(n1,n1),
inference(clausify,[status(thm)],[clause_2]) ).
cnf(c_4,plain,
f(n1,n1) = n2,
inference(copy,[status(thm)],[c_3]) ).
fof(clause_3,axiom,
n3 = f(n2,n1),
file('theBenchmark.p',clause_3) ).
cnf(c_5,plain,
n3 = f(n2,n1),
inference(clausify,[status(thm)],[clause_3]) ).
cnf(c_6,plain,
f(n2,n1) = n3,
inference(copy,[status(thm)],[c_5]) ).
fof(clause_4,axiom,
u = f(n2,n2),
file('theBenchmark.p',clause_4) ).
cnf(c_7,plain,
u = f(n2,n2),
inference(clausify,[status(thm)],[clause_4]) ).
cnf(c_8,plain,
f(n2,n2) = u,
inference(copy,[status(thm)],[c_7]) ).
fof(clause_5,axiom,
u1 = f(u,n1),
file('theBenchmark.p',clause_5) ).
cnf(c_9,plain,
u1 = f(u,n1),
inference(clausify,[status(thm)],[clause_5]) ).
cnf(c_10,plain,
f(u,n1) = u1,
inference(copy,[status(thm)],[c_9]) ).
fof(clause_6,axiom,
u2 = f(u,n2),
file('theBenchmark.p',clause_6) ).
cnf(c_11,plain,
u2 = f(u,n2),
inference(clausify,[status(thm)],[clause_6]) ).
cnf(c_12,plain,
f(u,n2) = u2,
inference(copy,[status(thm)],[c_11]) ).
fof(clause_7,axiom,
u3 = f(u,n3),
file('theBenchmark.p',clause_7) ).
cnf(c_13,plain,
u3 = f(u,n3),
inference(clausify,[status(thm)],[clause_7]) ).
cnf(c_14,plain,
f(u,n3) = u3,
inference(copy,[status(thm)],[c_13]) ).
fof(clause_8,axiom,
uu = f(u,u),
file('theBenchmark.p',clause_8) ).
cnf(c_15,plain,
uu = f(u,u),
inference(clausify,[status(thm)],[clause_8]) ).
cnf(c_16,plain,
f(u,u) = uu,
inference(copy,[status(thm)],[c_15]) ).
fof(clause_9,axiom,
a = f(f(n3,n2),u2),
file('theBenchmark.p',clause_9) ).
cnf(c_17,plain,
a = f(f(n3,n2),u2),
inference(clausify,[status(thm)],[clause_9]) ).
cnf(c_18,plain,
f(f(n3,n2),u2) = a,
inference(copy,[status(thm)],[c_17]) ).
fof(clause_10,axiom,
b = f(u1,u3),
file('theBenchmark.p',clause_10) ).
cnf(c_19,plain,
b = f(u1,u3),
inference(clausify,[status(thm)],[clause_10]) ).
cnf(c_20,plain,
f(u1,u3) = b,
inference(copy,[status(thm)],[c_19]) ).
fof(clause_11,axiom,
v = f(uu,uu),
file('theBenchmark.p',clause_11) ).
cnf(c_21,plain,
v = f(uu,uu),
inference(clausify,[status(thm)],[clause_11]) ).
cnf(c_22,plain,
f(uu,uu) = v,
inference(copy,[status(thm)],[c_21]) ).
fof(prove_equation,axiom,
f(a,v) != f(b,v),
file('theBenchmark.p',prove_equation) ).
cnf(c_23,plain,
f(a,v) != f(b,v),
inference(clausify,[status(thm)],[prove_equation]) ).
cnf(c_24,plain,
f(b,v) != f(a,v),
inference(copy,[status(thm)],[c_23]) ).
cnf(c_703,plain,
f(n2,f(n1,A)) = f(n1,f(n1,A)),
inference(paramod,[status(thm)],[c_4,c_2]) ).
cnf(c_27,plain,
f(n1,f(n1,A)) = f(n2,f(n1,A)),
inference(copy,[status(thm)],[c_703]) ).
cnf(c_29,plain,
f(n3,f(n2,A)) = f(n2,f(n1,A)),
inference(paramod,[status(thm)],[c_6,c_2]) ).
cnf(c_31,plain,
f(u,f(n2,A)) = f(n2,f(n2,A)),
inference(paramod,[status(thm)],[c_8,c_2]) ).
cnf(c_33,plain,
f(u1,f(u,A)) = f(u,f(n1,A)),
inference(paramod,[status(thm)],[c_10,c_2]) ).
cnf(c_704,plain,
f(u2,f(u,A)) = f(u,f(n2,A)),
inference(paramod,[status(thm)],[c_12,c_2]) ).
cnf(c_35,plain,
f(u2,f(u,A)) = f(n2,f(n2,A)),
inference(paramod,[status(thm)],[c_31,c_704]) ).
cnf(c_37,plain,
f(u3,f(u,A)) = f(u,f(n3,A)),
inference(paramod,[status(thm)],[c_14,c_2]) ).
cnf(c_39,plain,
f(uu,f(u,A)) = f(u,f(u,A)),
inference(paramod,[status(thm)],[c_16,c_2]) ).
cnf(c_705,plain,
f(a,f(f(n3,n2),A)) = f(f(n3,n2),f(u2,A)),
inference(paramod,[status(thm)],[c_18,c_2]) ).
cnf(c_41,plain,
f(f(n3,n2),f(u2,A)) = f(a,f(f(n3,n2),A)),
inference(copy,[status(thm)],[c_705]) ).
cnf(c_43,plain,
f(b,f(u1,A)) = f(u1,f(u3,A)),
inference(paramod,[status(thm)],[c_20,c_2]) ).
cnf(c_706,plain,
f(n1,n2) = f(n2,f(n1,n1)),
inference(paramod,[status(thm)],[c_4,c_27]) ).
cnf(c_707,plain,
f(n1,n2) = f(n2,n2),
inference(paramod,[status(thm)],[c_4,c_706]) ).
cnf(c_68,plain,
f(n1,n2) = u,
inference(paramod,[status(thm)],[c_8,c_707]) ).
cnf(c_708,plain,
f(n1,u) = f(n2,f(n1,n2)),
inference(paramod,[status(thm)],[c_68,c_27]) ).
cnf(c_74,plain,
f(n1,u) = f(n2,u),
inference(paramod,[status(thm)],[c_68,c_708]) ).
cnf(c_709,plain,
f(n3,u) = f(n2,f(n1,n2)),
inference(paramod,[status(thm)],[c_8,c_29]) ).
cnf(c_136,plain,
f(n3,u) = f(n2,u),
inference(paramod,[status(thm)],[c_68,c_709]) ).
cnf(c_146,plain,
f(f(n3,A),f(n2,u)) = f(n3,f(A,u)),
inference(paramod,[status(thm)],[c_136,c_2]) ).
cnf(c_710,plain,
f(u,u) = f(n2,f(n2,n2)),
inference(paramod,[status(thm)],[c_8,c_31]) ).
cnf(c_711,plain,
uu = f(n2,f(n2,n2)),
inference(paramod,[status(thm)],[c_16,c_710]) ).
cnf(c_712,plain,
uu = f(n2,u),
inference(paramod,[status(thm)],[c_8,c_711]) ).
cnf(c_152,plain,
f(n2,u) = uu,
inference(copy,[status(thm)],[c_712]) ).
cnf(c_159,plain,
f(f(n3,A),uu) = f(n3,f(A,u)),
inference(paramod,[status(thm)],[c_152,c_146]) ).
cnf(c_161,plain,
f(n3,u) = uu,
inference(paramod,[status(thm)],[c_152,c_136]) ).
cnf(c_176,plain,
f(n1,u) = uu,
inference(paramod,[status(thm)],[c_152,c_74]) ).
cnf(c_713,plain,
f(n3,uu) = f(n2,f(n1,u)),
inference(paramod,[status(thm)],[c_152,c_29]) ).
cnf(c_192,plain,
f(n3,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_176,c_713]) ).
cnf(c_714,plain,
f(u,uu) = f(n2,f(n2,u)),
inference(paramod,[status(thm)],[c_152,c_31]) ).
cnf(c_194,plain,
f(u,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_152,c_714]) ).
cnf(c_715,plain,
f(n1,uu) = f(n2,f(n1,u)),
inference(paramod,[status(thm)],[c_176,c_27]) ).
cnf(c_195,plain,
f(n1,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_176,c_715]) ).
cnf(c_211,plain,
f(f(n3,A),f(n2,uu)) = f(n3,f(A,uu)),
inference(paramod,[status(thm)],[c_192,c_2]) ).
cnf(c_716,plain,
f(u1,uu) = f(u,f(n1,u)),
inference(paramod,[status(thm)],[c_16,c_33]) ).
cnf(c_717,plain,
f(u1,uu) = f(u,uu),
inference(paramod,[status(thm)],[c_176,c_716]) ).
cnf(c_244,plain,
f(u1,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_194,c_717]) ).
cnf(c_718,plain,
f(u1,f(n2,uu)) = f(u,f(n1,uu)),
inference(paramod,[status(thm)],[c_194,c_33]) ).
cnf(c_719,plain,
f(u1,f(n2,uu)) = f(u,f(n2,uu)),
inference(paramod,[status(thm)],[c_195,c_718]) ).
cnf(c_252,plain,
f(u1,f(n2,uu)) = f(n2,f(n2,uu)),
inference(paramod,[status(thm)],[c_31,c_719]) ).
cnf(c_720,plain,
f(u2,uu) = f(n2,f(n2,u)),
inference(paramod,[status(thm)],[c_16,c_35]) ).
cnf(c_345,plain,
f(u2,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_152,c_720]) ).
cnf(c_721,plain,
f(u3,uu) = f(u,f(n3,u)),
inference(paramod,[status(thm)],[c_16,c_37]) ).
cnf(c_722,plain,
f(u3,uu) = f(u,uu),
inference(paramod,[status(thm)],[c_161,c_721]) ).
cnf(c_406,plain,
f(u3,uu) = f(n2,uu),
inference(paramod,[status(thm)],[c_194,c_722]) ).
cnf(c_723,plain,
f(uu,uu) = f(u,f(u,u)),
inference(paramod,[status(thm)],[c_16,c_39]) ).
cnf(c_724,plain,
v = f(u,f(u,u)),
inference(paramod,[status(thm)],[c_22,c_723]) ).
cnf(c_725,plain,
v = f(u,uu),
inference(paramod,[status(thm)],[c_16,c_724]) ).
cnf(c_726,plain,
v = f(n2,uu),
inference(paramod,[status(thm)],[c_194,c_725]) ).
cnf(c_463,plain,
f(n2,uu) = v,
inference(copy,[status(thm)],[c_726]) ).
cnf(c_476,plain,
f(u3,uu) = v,
inference(paramod,[status(thm)],[c_463,c_406]) ).
cnf(c_485,plain,
f(u2,uu) = v,
inference(paramod,[status(thm)],[c_463,c_345]) ).
cnf(c_727,plain,
f(u1,v) = f(n2,f(n2,uu)),
inference(paramod,[status(thm)],[c_463,c_252]) ).
cnf(c_493,plain,
f(u1,v) = f(n2,v),
inference(paramod,[status(thm)],[c_463,c_727]) ).
cnf(c_494,plain,
f(u1,uu) = v,
inference(paramod,[status(thm)],[c_463,c_244]) ).
cnf(c_512,plain,
f(f(n3,A),v) = f(n3,f(A,uu)),
inference(paramod,[status(thm)],[c_463,c_211]) ).
cnf(c_514,plain,
f(n1,uu) = v,
inference(paramod,[status(thm)],[c_463,c_195]) ).
cnf(c_516,plain,
f(n3,uu) = v,
inference(paramod,[status(thm)],[c_463,c_192]) ).
cnf(c_728,plain,
f(n3,v) = f(n2,f(n1,uu)),
inference(paramod,[status(thm)],[c_463,c_29]) ).
cnf(c_523,plain,
f(n3,v) = f(n2,v),
inference(paramod,[status(thm)],[c_514,c_728]) ).
cnf(c_729,plain,
f(f(n3,n2),v) = f(a,f(f(n3,n2),uu)),
inference(paramod,[status(thm)],[c_485,c_41]) ).
cnf(c_730,plain,
f(n3,f(n2,uu)) = f(a,f(f(n3,n2),uu)),
inference(paramod,[status(thm)],[c_512,c_729]) ).
cnf(c_731,plain,
f(n3,v) = f(a,f(f(n3,n2),uu)),
inference(paramod,[status(thm)],[c_463,c_730]) ).
cnf(c_732,plain,
f(n2,v) = f(a,f(f(n3,n2),uu)),
inference(paramod,[status(thm)],[c_523,c_731]) ).
cnf(c_733,plain,
f(n2,v) = f(a,f(n3,f(n2,u))),
inference(paramod,[status(thm)],[c_159,c_732]) ).
cnf(c_734,plain,
f(n2,v) = f(a,f(n3,uu)),
inference(paramod,[status(thm)],[c_152,c_733]) ).
cnf(c_735,plain,
f(n2,v) = f(a,v),
inference(paramod,[status(thm)],[c_516,c_734]) ).
cnf(c_575,plain,
f(a,v) = f(n2,v),
inference(copy,[status(thm)],[c_735]) ).
cnf(c_578,plain,
f(b,v) != f(n2,v),
inference(paramod,[status(thm)],[c_575,c_24]) ).
cnf(c_736,plain,
f(b,f(u1,uu)) = f(u1,v),
inference(paramod,[status(thm)],[c_476,c_43]) ).
cnf(c_737,plain,
f(b,v) = f(u1,v),
inference(paramod,[status(thm)],[c_494,c_736]) ).
cnf(c_738,plain,
f(b,v) = f(n2,v),
inference(paramod,[status(thm)],[c_493,c_737]) ).
cnf(c_702,plain,
$false,
inference(resolve,[status(thm)],[c_578,c_738]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LDA002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Fri Sep 25 23:55:00 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.38 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.11/0.38 % Process 2872542 was started by sandbox2 on n009,
% 0.11/0.38 % Fri Sep 25 23:55:00 2026
% 0.11/0.38 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.11/0.38
% 0.11/0.38 % From the command line: assign(max_seconds, 300).
% 0.75/0.52
% 0.75/0.52 % SZS status Unsatisfiable for theBenchmark
% 0.75/0.52
% 0.75/0.52 % Proof 1 at 0.08 (+ 0.03) seconds.
% 0.75/0.52 % Length of proof is 61.
% 0.75/0.52 % Level of proof is 11.
% 0.75/0.52 % Maximum clause weight is 55.000.
% 0.75/0.52 % Given clauses 98.
% 0.75/0.52
% 0.75/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------