%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : ALG210+2 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n026.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 : Fri Sep 25 12:52:05 PM UTC 2026
% Result : Theorem 7.19s 1.48s
% Output : Proof 7.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 4
% Syntax : Number of formulae : 85 ( 75 unt; 0 def)
% Number of atoms : 113 ( 89 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 44 ( 16 ~; 10 |; 15 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-4 aty)
% Number of variables : 68 ( 2 sgn 20 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [B] :
( element(B)
<=> ? [C] :
( times(B,B) = C
& times(B,C) = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_2) ).
fof(f1_nnf,plain,
! [B] :
( ( ! [C] :
( times(B,B) != C
| times(B,C) != B )
| element(B) )
& ( ? [C] :
( times(B,B) = C
& times(B,C) = B )
| ~ element(B) ) ),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [B,C] :
( ( times(B,B) != C
| times(B,C) != B
| element(B) )
& ( ( times(B,B) = sk0(B)
& times(B,sk0(B)) = B )
| ~ element(B) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f1_nnf]) ).
cnf(c3,plain,
( times(X0,X0) != X1
| times(X0,X1) != X0
| element(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t11,plain,
ifeq(times(X1,X2),X1,ifeq(times(X1,X1),X2,element(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t31,plain,
ifeq(times(X1,X2),X1,ifeq(times(X1,X1),X2,element(X1),true),true) = true,
inference(orient,[status(thm)],[t11]) ).
fof(f0,axiom,
! [A,B,C] : times(times(A,B),C) = times(B,times(C,A)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_1) ).
fof(f0_nnf,plain,
! [A,B,C] : times(times(A,B),C) = times(B,times(C,A)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,C] : times(times(A,B),C) = times(B,times(C,A)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
times(times(X0,X1),X2) = times(X1,times(X2,X0)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t9,plain,
times(times(X1,X2),X3) = times(X2,times(X3,X1)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t14,plain,
times(times(X1,X2),X3) = times(X2,times(X3,X1)),
inference(orient,[status(thm)],[t9]) ).
fof(f2,conjecture,
! [A,B,C] :
( ( C = times(A,B)
& element(B)
& element(A) )
=> element(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conjecture_1) ).
fof(f2_neg,negated_conjecture,
~ ! [A,B,C] :
( ( C = times(A,B)
& element(B)
& element(A) )
=> element(C) ),
inference(negated_conjecture,[status(cth)],[f2]) ).
fof(f2_nnf,plain,
? [A,B,C] :
( ~ element(C)
& C = times(A,B)
& element(B)
& element(A) ),
inference(nnf_transformation,[status(thm)],[f2_neg]) ).
fof(f2_sk,plain,
( ~ element(sk3)
& sk3 = times(sk1,sk2)
& element(sk2)
& element(sk1) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1,sk2,sk3])],[f2_nnf]) ).
cnf(c6,plain,
sk3 = times(sk1,sk2),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t2,plain,
times(sk1,sk2) = sk3,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t19,plain,
times(sk1,sk2) = sk3,
inference(orient,[status(thm)],[t2]) ).
cnf(t20,plain,
times(sk2,times(X1,sk1)) = times(sk3,X1),
inference(cp,[status(thm)],[t14,t19]) ).
cnf(t44,plain,
times(sk2,times(X1,sk1)) = times(sk3,X1),
inference(orient,[status(thm)],[t20]) ).
cnf(c2,plain,
( times(X0,X0) = sk0(X0)
| ~ element(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi2,axiom,
ifeq(element(X0),true,times(X0,X0),sk0(X0)) = sk0(X0),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(c4,plain,
element(sk1),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi4,negated_conjecture,
element(sk1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t4,plain,
times(sk1,sk1) = sk0(sk1),
inference(hyper_resolution,[status(thm)],[hi2,hi4]) ).
cnf(t17,plain,
times(sk1,sk1) = sk0(sk1),
inference(orient,[status(thm)],[t4]) ).
cnf(t46,plain,
times(sk3,sk1) = times(sk2,sk0(sk1)),
inference(cp,[status(thm)],[t44,t17]) ).
cnf(t49,plain,
times(sk2,sk0(sk1)) = times(sk3,sk1),
inference(orient,[status(thm)],[t46]) ).
cnf(t50,plain,
times(sk0(sk1),times(X1,sk2)) = times(times(sk3,sk1),X1),
inference(cp,[status(thm)],[t14,t49]) ).
cnf(t345,plain,
times(sk0(sk1),times(X1,sk2)) = times(sk1,times(X1,sk3)),
inference(step,[status(thm)],[t50,t14]) ).
cnf(t161,plain,
times(sk0(sk1),times(X1,sk2)) = times(sk1,times(X1,sk3)),
inference(orient,[status(thm)],[t345]) ).
cnf(t164,plain,
times(sk1,times(sk1,sk3)) = times(sk0(sk1),sk3),
inference(cp,[status(thm)],[t161,t19]) ).
cnf(t18,plain,
times(sk1,times(X1,sk1)) = times(sk0(sk1),X1),
inference(cp,[status(thm)],[t14,t17]) ).
cnf(t52,plain,
times(sk1,times(X1,sk1)) = times(sk0(sk1),X1),
inference(orient,[status(thm)],[t18]) ).
cnf(t54,plain,
times(sk0(sk1),sk1) = times(sk1,sk0(sk1)),
inference(cp,[status(thm)],[t52,t17]) ).
cnf(c1,plain,
( times(X0,sk0(X0)) = X0
| ~ element(X0) ),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
ifeq(element(X0),true,times(X0,sk0(X0)),X0) = X0,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t3,plain,
times(sk1,sk0(sk1)) = sk1,
inference(hyper_resolution,[status(thm)],[hi1,hi4]) ).
cnf(t21,plain,
times(sk1,sk0(sk1)) = sk1,
inference(orient,[status(thm)],[t3]) ).
cnf(t327,plain,
times(sk0(sk1),sk1) = sk1,
inference(step,[status(thm)],[t54,t21]) ).
cnf(t57,plain,
times(sk0(sk1),sk1) = sk1,
inference(orient,[status(thm)],[t327]) ).
cnf(t58,plain,
times(sk1,times(X1,sk0(sk1))) = times(sk1,X1),
inference(cp,[status(thm)],[t14,t57]) ).
cnf(t119,plain,
times(sk1,times(X1,sk0(sk1))) = times(sk1,X1),
inference(orient,[status(thm)],[t58]) ).
cnf(t121,plain,
times(sk1,sk2) = times(sk1,times(sk3,sk1)),
inference(cp,[status(thm)],[t119,t49]) ).
cnf(t341,plain,
sk3 = times(sk1,times(sk3,sk1)),
inference(step,[status(thm)],[t121,t19]) ).
cnf(t342,plain,
sk3 = times(sk0(sk1),sk3),
inference(step,[status(thm)],[t341,t52]) ).
cnf(t125,plain,
times(sk0(sk1),sk3) = sk3,
inference(orient,[status(thm)],[t342]) ).
cnf(t346,plain,
times(sk1,times(sk1,sk3)) = sk3,
inference(step,[status(thm)],[t164,t125]) ).
cnf(t167,plain,
times(sk1,times(sk1,sk3)) = sk3,
inference(orient,[status(thm)],[t346]) ).
cnf(t168,plain,
times(times(sk1,sk3),times(X1,sk1)) = times(sk3,X1),
inference(cp,[status(thm)],[t14,t167]) ).
cnf(t368,plain,
times(sk3,times(times(X1,sk1),sk1)) = times(sk3,X1),
inference(step,[status(thm)],[t168,t14]) ).
cnf(t369,plain,
times(sk3,times(sk1,times(sk1,X1))) = times(sk3,X1),
inference(step,[status(thm)],[t368,t14]) ).
cnf(t305,plain,
times(sk3,times(sk1,times(sk1,X1))) = times(sk3,X1),
inference(orient,[status(thm)],[t369]) ).
cnf(c5,plain,
element(sk2),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi5,negated_conjecture,
element(sk2) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t6,plain,
times(sk2,sk2) = sk0(sk2),
inference(hyper_resolution,[status(thm)],[hi2,hi5]) ).
cnf(t24,plain,
times(sk2,sk2) = sk0(sk2),
inference(orient,[status(thm)],[t6]) ).
cnf(t25,plain,
times(sk2,times(X1,sk2)) = times(sk0(sk2),X1),
inference(cp,[status(thm)],[t14,t24]) ).
cnf(t75,plain,
times(sk2,times(X1,sk2)) = times(sk0(sk2),X1),
inference(orient,[status(thm)],[t25]) ).
cnf(t78,plain,
times(sk0(sk2),sk1) = times(sk2,sk3),
inference(cp,[status(thm)],[t75,t19]) ).
cnf(t85,plain,
times(sk0(sk2),sk1) = times(sk2,sk3),
inference(orient,[status(thm)],[t78]) ).
cnf(t86,plain,
times(sk1,times(X1,sk0(sk2))) = times(times(sk2,sk3),X1),
inference(cp,[status(thm)],[t14,t85]) ).
cnf(t349,plain,
times(sk1,times(X1,sk0(sk2))) = times(sk3,times(X1,sk2)),
inference(step,[status(thm)],[t86,t14]) ).
cnf(t177,plain,
times(sk1,times(X1,sk0(sk2))) = times(sk3,times(X1,sk2)),
inference(orient,[status(thm)],[t349]) ).
cnf(t306,plain,
times(sk3,sk0(sk2)) = times(sk3,times(sk3,times(sk1,sk2))),
inference(cp,[status(thm)],[t305,t177]) ).
cnf(t5,plain,
times(sk2,sk0(sk2)) = sk2,
inference(hyper_resolution,[status(thm)],[hi1,hi5]) ).
cnf(t26,plain,
times(sk2,sk0(sk2)) = sk2,
inference(orient,[status(thm)],[t5]) ).
cnf(t180,plain,
times(sk3,times(sk2,sk2)) = times(sk1,sk2),
inference(cp,[status(thm)],[t177,t26]) ).
cnf(t350,plain,
times(sk3,sk0(sk2)) = times(sk1,sk2),
inference(step,[status(thm)],[t180,t24]) ).
cnf(t351,plain,
times(sk3,sk0(sk2)) = sk3,
inference(step,[status(thm)],[t350,t19]) ).
cnf(t184,plain,
times(sk3,sk0(sk2)) = sk3,
inference(orient,[status(thm)],[t351]) ).
cnf(t370,plain,
sk3 = times(sk3,times(sk3,times(sk1,sk2))),
inference(step,[status(thm)],[t306,t184]) ).
cnf(t371,plain,
sk3 = times(sk3,times(sk3,sk3)),
inference(step,[status(thm)],[t370,t19]) ).
cnf(t318,plain,
times(sk3,times(sk3,sk3)) = sk3,
inference(orient,[status(thm)],[t371]) ).
cnf(t320,plain,
true = ifeq(sk3,sk3,ifeq(times(sk3,sk3),times(sk3,sk3),element(sk3),true),true),
inference(cp,[status(thm)],[t31,t318]) ).
cnf(t7,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t12,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t372,plain,
true = ifeq(times(sk3,sk3),times(sk3,sk3),element(sk3),true),
inference(step,[status(thm)],[t320,t12]) ).
cnf(t373,plain,
true = element(sk3),
inference(step,[status(thm)],[t372,t12]) ).
cnf(t323,plain,
element(sk3) = true,
inference(orient,[status(thm)],[t373]) ).
cnf(c7,plain,
~ element(sk3),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(goal_0,negated_conjecture,
element(sk3) != true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t323]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG210+2 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n026.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Fri Sep 25 05:07:39 UTC 2026
% 0.02/0.37 % CPUTime :
% 0.02/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.19/1.48 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.19/1.48 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------