%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL031-2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n019.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:35:53 PM UTC 2026
% Result : Unsatisfiable 52.81s 7.76s
% Output : CNFRefutation 52.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 15
% Syntax : Number of clauses : 84 ( 84 unt; 0 nHn; 48 RR)
% Number of literals : 84 ( 83 equ; 4 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 70 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t11,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t73,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
cnf(t6,axiom,
join(composition(converse(sk2),sk2),one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t18187,plain,
join(one,composition(converse(sk2),sk2)) = one,
inference(step,[status(thm)],[t6,t71]) ).
cnf(t94,plain,
join(one,composition(converse(sk2),sk2)) = one,
inference(orient,[status(thm)],[t18187]) ).
cnf(t95,plain,
join(one,join(composition(converse(sk2),sk2),X1)) = join(one,X1),
inference(cp,[status(thm)],[t73,t94]) ).
cnf(t1931,plain,
join(one,join(composition(converse(sk2),sk2),X1)) = join(one,X1),
inference(orient,[status(thm)],[t95]) ).
cnf(t12,axiom,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t35,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
cnf(t1932,plain,
join(one,composition(X1,sk2)) = join(one,composition(join(converse(sk2),X1),sk2)),
inference(cp,[status(thm)],[t1931,t35]) ).
cnf(t18060,plain,
join(one,composition(join(converse(sk2),X1),sk2)) = join(one,composition(X1,sk2)),
inference(orient,[status(thm)],[t1932]) ).
cnf(t9,axiom,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t8,axiom,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t29,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
cnf(t1,axiom,
converse(converse(X1)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t31,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t29,t23]) ).
cnf(t293,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t31]) ).
cnf(t303,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(cp,[status(thm)],[t66,t293]) ).
cnf(t5170,plain,
converse(join(X1,composition(converse(X2),X3))) = join(converse(X1),composition(converse(X3),X2)),
inference(orient,[status(thm)],[t303]) ).
cnf(t10,axiom,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t27,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
cnf(t41,plain,
composition(join(X1,composition(X2,X3)),Y3) = join(composition(X1,Y3),composition(X2,composition(X3,Y3))),
inference(cp,[status(thm)],[t35,t27]) ).
cnf(t8218,plain,
join(composition(X1,X2),composition(X3,composition(Y3,X2))) = composition(join(X1,composition(X3,Y3)),X2),
inference(orient,[status(thm)],[t41]) ).
cnf(t18,axiom,
sFlat0 = composition(sk1,sk2),
introduced(definition) ).
cnf(t54,plain,
composition(sk1,sk2) = sFlat0,
inference(orient,[status(thm)],[t18]) ).
cnf(t8307,plain,
composition(join(X1,composition(X2,sk1)),sk2) = join(composition(X1,sk2),composition(X2,sFlat0)),
inference(cp,[status(thm)],[t8218,t54]) ).
cnf(t8985,plain,
composition(join(X1,composition(X2,sk1)),sk2) = join(composition(X1,sk2),composition(X2,sFlat0)),
inference(orient,[status(thm)],[t8307]) ).
cnf(t5,axiom,
join(composition(converse(sk1),sk1),one) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18186,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(step,[status(thm)],[t5,t71]) ).
cnf(t92,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(orient,[status(thm)],[t18186]) ).
cnf(t8987,plain,
join(composition(one,sk2),composition(converse(sk1),sFlat0)) = composition(one,sk2),
inference(cp,[status(thm)],[t8985,t92]) ).
cnf(t0,axiom,
composition(X1,one) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t294,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t293,t22]) ).
cnf(t18201,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t294,t23]) ).
cnf(t311,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t18201]) ).
cnf(t28,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(cp,[status(thm)],[t27,t22]) ).
cnf(t263,plain,
composition(X1,composition(one,X2)) = composition(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t313,plain,
composition(one,X1) = composition(converse(one),X1),
inference(cp,[status(thm)],[t311,t263]) ).
cnf(t18203,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t313,t311]) ).
cnf(t332,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t18203]) ).
cnf(t18440,plain,
join(sk2,composition(converse(sk1),sFlat0)) = composition(one,sk2),
inference(step,[status(thm)],[t8987,t332]) ).
cnf(t18441,plain,
join(sk2,composition(converse(sk1),sFlat0)) = sk2,
inference(step,[status(thm)],[t18440,t332]) ).
cnf(t9011,plain,
join(sk2,composition(converse(sk1),sFlat0)) = sk2,
inference(orient,[status(thm)],[t18441]) ).
cnf(t9014,plain,
join(converse(sk2),composition(converse(sFlat0),sk1)) = converse(sk2),
inference(cp,[status(thm)],[t5170,t9011]) ).
cnf(t19,axiom,
sFlat1 = converse(composition(sk1,sk2)),
introduced(definition) ).
cnf(t18180,plain,
sFlat1 = converse(sFlat0),
inference(step,[status(thm)],[t19,t54]) ).
cnf(t60,plain,
converse(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t18180]) ).
cnf(t18442,plain,
join(converse(sk2),composition(sFlat1,sk1)) = converse(sk2),
inference(step,[status(thm)],[t9014,t60]) ).
cnf(t9015,plain,
join(converse(sk2),composition(sFlat1,sk1)) = converse(sk2),
inference(orient,[status(thm)],[t18442]) ).
cnf(t18063,plain,
join(one,composition(composition(sFlat1,sk1),sk2)) = join(one,composition(converse(sk2),sk2)),
inference(cp,[status(thm)],[t18060,t9015]) ).
cnf(t18688,plain,
join(one,composition(sFlat1,composition(sk1,sk2))) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t18063,t27]) ).
cnf(t18689,plain,
join(one,composition(sFlat1,sFlat0)) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t18688,t54]) ).
cnf(t20,axiom,
sFlat2 = composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),
introduced(definition) ).
cnf(t33,plain,
composition(converse(composition(sk1,sk2)),composition(sk1,sk2)) = sFlat2,
inference(orient,[status(thm)],[t20]) ).
cnf(t18178,plain,
composition(converse(sFlat0),composition(sk1,sk2)) = sFlat2,
inference(step,[status(thm)],[t33,t54]) ).
cnf(t18179,plain,
composition(converse(sFlat0),sFlat0) = sFlat2,
inference(step,[status(thm)],[t18178,t54]) ).
cnf(t59,plain,
composition(converse(sFlat0),sFlat0) = sFlat2,
inference(rw,[status(thm)],[t18179]) ).
cnf(t18192,plain,
composition(sFlat1,sFlat0) = sFlat2,
inference(step,[status(thm)],[t59,t60]) ).
cnf(t155,plain,
composition(sFlat1,sFlat0) = sFlat2,
inference(orient,[status(thm)],[t18192]) ).
cnf(t18690,plain,
join(one,sFlat2) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t18689,t155]) ).
cnf(t18691,plain,
join(sFlat2,one) = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t18690,t71]) ).
cnf(t21,axiom,
sFlat3 = join(composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),one),
introduced(definition) ).
cnf(t18182,plain,
sFlat3 = join(one,composition(converse(composition(sk1,sk2)),composition(sk1,sk2))),
inference(step,[status(thm)],[t21,t71]) ).
cnf(t18183,plain,
sFlat3 = join(one,composition(converse(sFlat0),composition(sk1,sk2))),
inference(step,[status(thm)],[t18182,t54]) ).
cnf(t18184,plain,
sFlat3 = join(one,composition(sFlat1,composition(sk1,sk2))),
inference(step,[status(thm)],[t18183,t60]) ).
cnf(t18185,plain,
sFlat3 = join(one,composition(sFlat1,sFlat0)),
inference(step,[status(thm)],[t18184,t54]) ).
cnf(t90,plain,
join(one,composition(sFlat1,sFlat0)) = sFlat3,
inference(orient,[status(thm)],[t18185]) ).
cnf(t18193,plain,
join(one,sFlat2) = sFlat3,
inference(step,[status(thm)],[t90,t155]) ).
cnf(t161,plain,
join(one,sFlat2) = sFlat3,
inference(rw,[status(thm)],[t18193]) ).
cnf(t18194,plain,
join(sFlat2,one) = sFlat3,
inference(step,[status(thm)],[t161,t71]) ).
cnf(t162,plain,
join(sFlat2,one) = sFlat3,
inference(orient,[status(thm)],[t18194]) ).
cnf(t18692,plain,
sFlat3 = join(one,composition(converse(sk2),sk2)),
inference(step,[status(thm)],[t18691,t162]) ).
cnf(t18693,plain,
sFlat3 = one,
inference(step,[status(thm)],[t18692,t94]) ).
cnf(t18115,plain,
one = sFlat3,
inference(orient,[status(thm)],[t18693]) ).
cnf(goal_0,negated_conjecture,
join(composition(converse(composition(sk1,sk2)),composition(sk1,sk2)),one) != one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(sFlat2,one) != one,
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
sFlat3 != one,
inference(rw,[status(thm)],[g0_0]) ).
cnf(g0_2,plain,
sFlat3 != sFlat3,
inference(rw,[status(thm)],[g0_1,t18115]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL031-2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n019.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 07:26:49 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 52.81/7.76 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 52.81/7.76 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------