%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL009-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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 02:34:41 PM UTC 2026
% Result : Unsatisfiable 21.51s 8.51s
% Output : Proof 21.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 12
% Syntax : Number of formulae : 99 ( 95 unt; 0 def)
% Number of atoms : 103 ( 102 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 15 ( 11 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 12 con; 0-4 aty)
% Number of variables : 41 ( 2 sgn 10 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f17,negated_conjecture,
( join(composition(sk3,sk1),composition(sk3,sk2)) != composition(sk3,sk2)
| join(composition(sk1,sk3),composition(sk2,sk3)) != composition(sk2,sk3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_18) ).
fof(f17_nnf,plain,
( join(composition(sk3,sk1),composition(sk3,sk2)) != composition(sk3,sk2)
| join(composition(sk1,sk3),composition(sk2,sk3)) != composition(sk2,sk3) ),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
( join(composition(sk3,sk1),composition(sk3,sk2)) != composition(sk3,sk2)
| join(composition(sk1,sk3),composition(sk2,sk3)) != composition(sk2,sk3) ),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
( join(composition(sk3,sk1),composition(sk3,sk2)) != composition(sk3,sk2)
| join(composition(sk1,sk3),composition(sk2,sk3)) != composition(sk2,sk3) ),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t14,plain,
ifeq(join(composition(sk1,sk3),composition(sk2,sk3)),composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(f6,axiom,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',composition_distributivity_7) ).
fof(f6_nnf,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A,B,C] : composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t144,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t9341,plain,
ifeq(composition(join(sk1,sk2),sk3),composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t14,t144]) ).
cnf(t19,axiom,
sF1 = composition(sk1,sk3),
introduced(definition) ).
cnf(t32,plain,
composition(sk1,sk3) = sF1,
inference(orient,[status(thm)],[t19]) ).
cnf(t145,plain,
composition(join(sk1,X1),sk3) = join(sF1,composition(X1,sk3)),
inference(cp,[status(thm)],[t144,t32]) ).
cnf(t266,plain,
composition(join(sk1,X1),sk3) = join(sF1,composition(X1,sk3)),
inference(orient,[status(thm)],[t145]) ).
cnf(t9342,plain,
ifeq(join(sF1,composition(sk2,sk3)),composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9341,t266]) ).
cnf(t18,axiom,
sF0 = join(sk1,sk2),
introduced(definition) ).
cnf(f16,negated_conjecture,
join(sk1,sk2) = sk2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_17) ).
fof(f16_nnf,plain,
join(sk1,sk2) = sk2,
inference(nnf_transformation,[status(thm)],[f16]) ).
cnf(c16,plain,
join(sk1,sk2) = sk2,
inference(cnf_transformation,[status(esa)],[f16_nnf]) ).
cnf(t2,plain,
join(sk1,sk2) = sk2,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t29,plain,
join(sk1,sk2) = sk2,
inference(orient,[status(thm)],[t2]) ).
cnf(t9318,plain,
sF0 = sk2,
inference(step,[status(thm)],[t18,t29]) ).
cnf(t30,plain,
sk2 = sF0,
inference(orient,[status(thm)],[t9318]) ).
cnf(t9343,plain,
ifeq(join(sF1,composition(sF0,sk3)),composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9342,t30]) ).
cnf(t20,axiom,
sF2 = composition(sk2,sk3),
introduced(definition) ).
cnf(t9319,plain,
sF2 = composition(sF0,sk3),
inference(step,[status(thm)],[t20,t30]) ).
cnf(t33,plain,
composition(sF0,sk3) = sF2,
inference(orient,[status(thm)],[t9319]) ).
cnf(t9344,plain,
ifeq(join(sF1,sF2),composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9343,t33]) ).
cnf(t146,plain,
composition(join(X1,sk1),sk3) = join(composition(X1,sk3),sF1),
inference(cp,[status(thm)],[t144,t32]) ).
cnf(f0,axiom,
join(A,B) = join(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',maddux1_join_commutativity_1) ).
fof(f0_nnf,plain,
! [A,B] : join(A,B) = join(B,A),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : join(A,B) = join(B,A),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t74,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t9334,plain,
composition(join(X1,sk1),sk3) = join(sF1,composition(X1,sk3)),
inference(step,[status(thm)],[t146,t74]) ).
cnf(t272,plain,
composition(join(X1,sk1),sk3) = join(sF1,composition(X1,sk3)),
inference(orient,[status(thm)],[t9334]) ).
cnf(t31,plain,
join(sk1,sF0) = sk2,
inference(rw,[status(thm)],[t29]) ).
cnf(t9321,plain,
join(sk1,sF0) = sF0,
inference(step,[status(thm)],[t31,t30]) ).
cnf(t36,plain,
join(sk1,sF0) = sF0,
inference(orient,[status(thm)],[t9321]) ).
cnf(t9324,plain,
join(sF0,sk1) = sF0,
inference(step,[status(thm)],[t36,t74]) ).
cnf(t75,plain,
join(sF0,sk1) = sF0,
inference(rw,[status(thm)],[t9324]) ).
cnf(t80,plain,
join(sF0,sk1) = sF0,
inference(orient,[status(thm)],[t75]) ).
cnf(t274,plain,
join(sF1,composition(sF0,sk3)) = composition(sF0,sk3),
inference(cp,[status(thm)],[t272,t80]) ).
cnf(t9335,plain,
join(sF1,sF2) = composition(sF0,sk3),
inference(step,[status(thm)],[t274,t33]) ).
cnf(t9336,plain,
join(sF1,sF2) = sF2,
inference(step,[status(thm)],[t9335,t33]) ).
cnf(t279,plain,
join(sF1,sF2) = sF2,
inference(orient,[status(thm)],[t9336]) ).
cnf(t9345,plain,
ifeq(sF2,composition(sk2,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9344,t279]) ).
cnf(t9346,plain,
ifeq(sF2,composition(sF0,sk3),ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9345,t30]) ).
cnf(t9347,plain,
ifeq(sF2,sF2,ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),true) = true,
inference(step,[status(thm)],[t9346,t33]) ).
cnf(t4,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t38,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t9348,plain,
ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9347,t38]) ).
cnf(t9349,plain,
ifeq(join(composition(sk3,sk2),composition(sk3,sk1)),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9348,t74]) ).
cnf(t9350,plain,
ifeq(join(composition(sk3,sF0),composition(sk3,sk1)),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9349,t30]) ).
cnf(t23,axiom,
sF5 = composition(sk3,sk2),
introduced(definition) ).
cnf(t9320,plain,
sF5 = composition(sk3,sF0),
inference(step,[status(thm)],[t23,t30]) ).
cnf(t35,plain,
composition(sk3,sF0) = sF5,
inference(orient,[status(thm)],[t9320]) ).
cnf(t9351,plain,
ifeq(join(sF5,composition(sk3,sk1)),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9350,t35]) ).
cnf(t22,axiom,
sF4 = composition(sk3,sk1),
introduced(definition) ).
cnf(t34,plain,
composition(sk3,sk1) = sF4,
inference(orient,[status(thm)],[t22]) ).
cnf(t9352,plain,
ifeq(join(sF5,sF4),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9351,t34]) ).
cnf(t9353,plain,
ifeq(join(sF4,sF5),composition(sk3,sk2),false,true) = true,
inference(step,[status(thm)],[t9352,t74]) ).
cnf(t9354,plain,
ifeq(join(sF4,sF5),composition(sk3,sF0),false,true) = true,
inference(step,[status(thm)],[t9353,t30]) ).
cnf(t9355,plain,
ifeq(join(sF4,sF5),sF5,false,true) = true,
inference(step,[status(thm)],[t9354,t35]) ).
cnf(t334,plain,
ifeq(join(sF4,sF5),sF5,false,true) = true,
inference(orient,[status(thm)],[t9355]) ).
cnf(t24,axiom,
sF6 = join(composition(sk3,sk1),composition(sk3,sk2)),
introduced(definition) ).
cnf(t9400,plain,
sF6 = join(composition(sk3,sk2),composition(sk3,sk1)),
inference(step,[status(thm)],[t24,t74]) ).
cnf(t9401,plain,
sF6 = join(composition(sk3,sF0),composition(sk3,sk1)),
inference(step,[status(thm)],[t9400,t30]) ).
cnf(t9402,plain,
sF6 = join(sF5,composition(sk3,sk1)),
inference(step,[status(thm)],[t9401,t35]) ).
cnf(t9403,plain,
sF6 = join(sF5,sF4),
inference(step,[status(thm)],[t9402,t34]) ).
cnf(t9404,plain,
sF6 = join(sF4,sF5),
inference(step,[status(thm)],[t9403,t74]) ).
cnf(t664,plain,
join(sF4,sF5) = sF6,
inference(orient,[status(thm)],[t9404]) ).
cnf(t9405,plain,
ifeq(sF6,sF5,false,true) = true,
inference(step,[status(thm)],[t334,t664]) ).
cnf(t665,plain,
ifeq(sF6,sF5,false,true) = true,
inference(rw,[status(thm)],[t9405]) ).
cnf(t25,axiom,
sF7 = ifeq(join(composition(sk3,sk1),composition(sk3,sk2)),composition(sk3,sk2),false,true),
introduced(definition) ).
cnf(t9407,plain,
sF7 = ifeq(join(composition(sk3,sk2),composition(sk3,sk1)),composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t25,t74]) ).
cnf(t9408,plain,
sF7 = ifeq(join(composition(sk3,sF0),composition(sk3,sk1)),composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t9407,t30]) ).
cnf(t9409,plain,
sF7 = ifeq(join(sF5,composition(sk3,sk1)),composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t9408,t35]) ).
cnf(t9410,plain,
sF7 = ifeq(join(sF5,sF4),composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t9409,t34]) ).
cnf(t9411,plain,
sF7 = ifeq(join(sF4,sF5),composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t9410,t74]) ).
cnf(t9412,plain,
sF7 = ifeq(sF6,composition(sk3,sk2),false,true),
inference(step,[status(thm)],[t9411,t664]) ).
cnf(t9413,plain,
sF7 = ifeq(sF6,composition(sk3,sF0),false,true),
inference(step,[status(thm)],[t9412,t30]) ).
cnf(t9414,plain,
sF7 = ifeq(sF6,sF5,false,true),
inference(step,[status(thm)],[t9413,t35]) ).
cnf(t708,plain,
ifeq(sF6,sF5,false,true) = sF7,
inference(orient,[status(thm)],[t9414]) ).
cnf(t9451,plain,
sF7 = true,
inference(step,[status(thm)],[t665,t708]) ).
cnf(t872,plain,
true = sF7,
inference(orient,[status(thm)],[t9451]) ).
cnf(t9452,plain,
ifeq(sF6,sF5,false,sF7) = sF7,
inference(step,[status(thm)],[t708,t872]) ).
cnf(t873,plain,
ifeq(sF6,sF5,false,sF7) = sF7,
inference(rw,[status(thm)],[t9452]) ).
cnf(t1031,plain,
ifeq(sF6,sF5,false,sF7) = sF7,
inference(orient,[status(thm)],[t873]) ).
cnf(t9135,plain,
ifeq(sF5,sF5,false,sF7) = sF7,
inference(rw,[status(thm)],[t1031]) ).
cnf(t9768,plain,
false = sF7,
inference(step,[status(thm)],[t9135,t38]) ).
cnf(t9317,plain,
false = sF7,
inference(orient,[status(thm)],[t9768]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
sF7 != false,
inference(rw,[status(thm)],[goal_0,t872]) ).
cnf(g0_1,plain,
sF7 != sF7,
inference(rw,[status(thm)],[g0_0,t9317]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL009-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/5.39 % Computer : n008.cluster.edu
% 0.11/5.39 % Model : x86_64 x86_64
% 0.11/5.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.39 % Memory : 8046.5625MB
% 0.11/5.39 % OS : Linux 6.8.0-71-generic
% 0.11/5.39 % CPULimit : 300
% 0.11/5.39 % WCLimit : 300
% 0.11/5.39 % DateTime : Thu Sep 24 07:08:50 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 21.51/8.51 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 21.51/8.51 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------