%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL903+1 : TPTP v9.3.1. Released v5.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:03:19 PM UTC 2026
% Result : Theorem 43.02s 5.88s
% Output : Proof 43.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 15
% Syntax : Number of formulae : 207 ( 182 unt; 0 def)
% Number of atoms : 244 ( 177 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 70 ( 33 ~; 27 |; 4 &)
% ( 1 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 1 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 : 397 ( 50 sgn 83 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X5,X6,X7] :
( qtd2(qtd0(X5,X6),X7)
<=> qtd2(X6,qtd3(X5,X7)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_07) ).
fof(f6_nnf,plain,
! [X5,X6,X7] :
( ( ~ qtd2(X6,qtd3(X5,X7))
| qtd2(qtd0(X5,X6),X7) )
& ( qtd2(X6,qtd3(X5,X7))
| ~ qtd2(qtd0(X5,X6),X7) ) ),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X5,X6,X7] :
( ( ~ qtd2(X6,qtd3(X5,X7))
| qtd2(qtd0(X5,X6),X7) )
& ( qtd2(X6,qtd3(X5,X7))
| ~ qtd2(qtd0(X5,X6),X7) ) ),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
( qtd2(X1,qtd3(X0,X2))
| ~ qtd2(qtd0(X0,X1),X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi6,axiom,
ifeq(qtd2(qtd0(X0,X1),X2),true,qtd2(X1,qtd3(X0,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
fof(f3,axiom,
! [A] : qtd2(A,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_04) ).
fof(f3_nnf,plain,
! [A] : qtd2(A,A),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A] : qtd2(A,A),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
qtd2(X0,X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(hi3,axiom,
qtd2(X0,X0) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(h3,plain,
qtd2(V0,qtd3(V1,qtd0(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi3]) ).
fof(f4,axiom,
! [X0,X1,X2] :
( ( qtd2(X1,X2)
& qtd2(X0,X1) )
=> qtd2(X0,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_05) ).
fof(f4_nnf,plain,
! [X0,X1,X2] :
( qtd2(X0,X2)
| ~ qtd2(X1,X2)
| ~ qtd2(X0,X1) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2] :
( qtd2(X0,X2)
| ~ qtd2(X1,X2)
| ~ qtd2(X0,X1) ),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
( qtd2(X0,X2)
| ~ qtd2(X1,X2)
| ~ qtd2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
ifeq(qtd2(X0,X1),true,ifeq(qtd2(X1,X2),true,qtd2(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(h40,plain,
qtd2(V0,qtd3(V1,qtd0(V1,qtd3(V2,qtd0(V2,V0))))) = true,
inference(hyper_resolution,[status(thm)],[hi4,h3,h3]) ).
cnf(c7,plain,
( ~ qtd2(X1,qtd3(X0,X2))
| qtd2(qtd0(X0,X1),X2) ),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi7,axiom,
ifeq(qtd2(X0,qtd3(X1,X2)),true,qtd2(qtd0(X1,X0),X2),true) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(h548,plain,
qtd2(qtd0(V0,V1),qtd0(V0,qtd3(V2,qtd0(V2,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi7,h40]) ).
fof(f8,axiom,
! [X8,X9,X10] :
( qtd2(X8,X9)
=> qtd2(qtd0(X8,X10),qtd0(X9,X10)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_09) ).
fof(f8_nnf,plain,
! [X8,X9,X10] :
( qtd2(qtd0(X8,X10),qtd0(X9,X10))
| ~ qtd2(X8,X9) ),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X8,X9,X10] :
( qtd2(qtd0(X8,X10),qtd0(X9,X10))
| ~ qtd2(X8,X9) ),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c9,plain,
( qtd2(qtd0(X0,X2),qtd0(X1,X2))
| ~ qtd2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(hi9,axiom,
ifeq(qtd2(X0,X1),true,qtd2(qtd0(X0,X2),qtd0(X1,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(h1,plain,
qtd2(qtd0(V0,V1),qtd0(V0,V1)) = true,
inference(hyper_resolution,[status(thm)],[hi9,hi3]) ).
cnf(h2,plain,
qtd2(qtd0(V0,qtd3(V0,V1)),V1) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3]) ).
cnf(h30,plain,
qtd2(qtd0(V0,qtd3(V0,qtd0(V1,V2))),qtd0(V1,V2)) = true,
inference(hyper_resolution,[status(thm)],[hi4,h2,h1]) ).
fof(f5,axiom,
! [X3,X4] :
( ( qtd2(X4,X3)
& qtd2(X3,X4) )
=> X3 = X4 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_06) ).
fof(f5_nnf,plain,
! [X3,X4] :
( X3 = X4
| ~ qtd2(X4,X3)
| ~ qtd2(X3,X4) ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X3,X4] :
( X3 = X4
| ~ qtd2(X4,X3)
| ~ qtd2(X3,X4) ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( X0 = X1
| ~ qtd2(X1,X0)
| ~ qtd2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(hi5,axiom,
ifeq(qtd2(X0,X1),true,ifeq(qtd2(X1,X0),true,X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t34,plain,
qtd0(X1,qtd3(X1,qtd0(X1,X2))) = qtd0(X1,X2),
inference(hyper_resolution,[status(thm)],[hi5,h30,h548]) ).
cnf(t376,plain,
qtd0(X1,qtd3(X1,qtd0(X1,X2))) = qtd0(X1,X2),
inference(orient,[status(thm)],[t34]) ).
fof(f1,axiom,
! [A,B] : qtd0(A,B) = qtd0(B,A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_02) ).
fof(f1_nnf,plain,
! [A,B] : qtd0(A,B) = qtd0(B,A),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B] : qtd0(A,B) = qtd0(B,A),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
qtd0(X0,X1) = qtd0(X1,X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t6,plain,
qtd0(X1,X2) = qtd0(X2,X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t368,plain,
qtd0(X1,X2) = qtd0(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t377,plain,
qtd0(X1,X2) = qtd0(X1,qtd3(X1,qtd0(X2,X1))),
inference(cp,[status(thm)],[t376,t368]) ).
cnf(t1595,plain,
qtd0(X1,qtd3(X1,qtd0(X2,X1))) = qtd0(X1,X2),
inference(orient,[status(thm)],[t377]) ).
cnf(t136,plain,
ifeq(qtd2(X1,X2),true,ifeq(qtd2(X2,X1),true,X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t258,plain,
ifeq(qtd2(X1,X2),true,ifeq(qtd2(X2,X1),true,X1,X2),X2) = X2,
inference(orient,[status(thm)],[t136]) ).
fof(f9,axiom,
! [X11,X12,X13] :
( qtd2(X11,X12)
=> qtd2(qtd3(X12,X13),qtd3(X11,X13)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_10) ).
fof(f9_nnf,plain,
! [X11,X12,X13] :
( qtd2(qtd3(X12,X13),qtd3(X11,X13))
| ~ qtd2(X11,X12) ),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X11,X12,X13] :
( qtd2(qtd3(X12,X13),qtd3(X11,X13))
| ~ qtd2(X11,X12) ),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c10,plain,
( qtd2(qtd3(X1,X2),qtd3(X0,X2))
| ~ qtd2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(hi10,axiom,
ifeq(qtd2(X0,X1),true,qtd2(qtd3(X1,X2),qtd3(X0,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t122,plain,
qtd2(qtd3(qtd3(X1,qtd0(X1,X2)),X3),qtd3(X2,X3)) = true,
inference(hyper_resolution,[status(thm)],[hi10,h3]) ).
cnf(t517,plain,
qtd2(qtd3(qtd3(X1,qtd0(X1,X2)),X3),qtd3(X2,X3)) = true,
inference(orient,[status(thm)],[t122]) ).
cnf(t15,plain,
qtd2(qtd0(X1,qtd3(X1,X2)),X2) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3]) ).
cnf(t556,plain,
qtd2(qtd0(X1,qtd3(X1,X2)),X2) = true,
inference(orient,[status(thm)],[t15]) ).
fof(f12,axiom,
! [A] : qtd3(qtd3(qtd3(A,qtd4),A),A) = qtd1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f12_nnf,plain,
! [A] : qtd3(qtd3(qtd3(A,qtd4),A),A) = qtd1,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A] : qtd3(qtd3(qtd3(A,qtd4),A),A) = qtd1,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
qtd3(qtd3(qtd3(X0,qtd4),X0),X0) = qtd1,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t33,plain,
qtd3(qtd3(qtd3(X1,qtd4),X1),X1) = qtd1,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t329,plain,
qtd3(qtd3(qtd3(X1,qtd4),X1),X1) = qtd1,
inference(orient,[status(thm)],[t33]) ).
cnf(t559,plain,
true = qtd2(qtd0(qtd3(qtd3(X1,qtd4),X1),qtd1),X1),
inference(cp,[status(thm)],[t556,t329]) ).
fof(f2,axiom,
! [A] : qtd0(A,qtd1) = A,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_03) ).
fof(f2_nnf,plain,
! [A] : qtd0(A,qtd1) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : qtd0(A,qtd1) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
qtd0(X0,qtd1) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t0,plain,
qtd0(X1,qtd1) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t256,plain,
qtd0(X1,qtd1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t14391,plain,
true = qtd2(qtd3(qtd3(X1,qtd4),X1),X1),
inference(step,[status(thm)],[t559,t256]) ).
cnf(t1119,plain,
qtd2(qtd3(qtd3(X1,qtd4),X1),X1) = true,
inference(orient,[status(thm)],[t14391]) ).
cnf(t1120,plain,
X1 = ifeq(true,true,ifeq(qtd2(X1,qtd3(qtd3(X1,qtd4),X1)),true,qtd3(qtd3(X1,qtd4),X1),X1),X1),
inference(cp,[status(thm)],[t258,t1119]) ).
cnf(t5,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t257,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t5]) ).
cnf(t14392,plain,
X1 = ifeq(qtd2(X1,qtd3(qtd3(X1,qtd4),X1)),true,qtd3(qtd3(X1,qtd4),X1),X1),
inference(step,[status(thm)],[t1120,t257]) ).
cnf(h25,plain,
qtd2(qtd3(V0,V1),qtd3(qtd0(V2,qtd3(V2,V0)),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi10,h2]) ).
cnf(t94,plain,
qtd2(X1,qtd3(qtd0(X2,qtd3(X2,X3)),qtd0(X3,X1))) = true,
inference(hyper_resolution,[status(thm)],[hi4,h3,h25]) ).
cnf(t459,plain,
qtd2(X1,qtd3(qtd0(X2,qtd3(X2,X3)),qtd0(X3,X1))) = true,
inference(orient,[status(thm)],[t94]) ).
cnf(t369,plain,
qtd0(qtd1,X1) = X1,
inference(cp,[status(thm)],[t368,t256]) ).
cnf(t882,plain,
qtd0(qtd1,X1) = X1,
inference(orient,[status(thm)],[t369]) ).
cnf(t908,plain,
true = qtd2(X1,qtd3(qtd0(X2,qtd3(X2,qtd1)),X1)),
inference(cp,[status(thm)],[t459,t882]) ).
cnf(h36,plain,
qtd2(V0,qtd3(V1,qtd3(V2,qtd0(V2,qtd0(V1,V0))))) = true,
inference(hyper_resolution,[status(thm)],[hi6,h3]) ).
fof(f10,axiom,
! [X14,X15,X16] :
( qtd2(X14,X15)
=> qtd2(qtd3(X16,X14),qtd3(X16,X15)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_11) ).
fof(f10_nnf,plain,
! [X14,X15,X16] :
( qtd2(qtd3(X16,X14),qtd3(X16,X15))
| ~ qtd2(X14,X15) ),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X14,X15,X16] :
( qtd2(qtd3(X16,X14),qtd3(X16,X15))
| ~ qtd2(X14,X15) ),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c11,plain,
( qtd2(qtd3(X2,X0),qtd3(X2,X1))
| ~ qtd2(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(hi11,axiom,
ifeq(qtd2(X0,X1),true,qtd2(qtd3(X2,X0),qtd3(X2,X1)),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(h0,plain,
qtd2(qtd3(V0,V1),qtd3(V0,V1)) = true,
inference(hyper_resolution,[status(thm)],[hi11,hi3]) ).
fof(f7,axiom,
! [A] : qtd2(A,qtd1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_08) ).
fof(f7_nnf,plain,
! [A] : qtd2(A,qtd1),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A] : qtd2(A,qtd1),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c8,plain,
qtd2(X0,qtd1),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(hi8,axiom,
qtd2(X0,qtd1) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(h11,plain,
qtd2(qtd3(V0,V1),qtd1) = true,
inference(hyper_resolution,[status(thm)],[hi4,h0,hi8]) ).
cnf(t55,plain,
qtd3(X1,qtd3(X2,qtd0(X2,qtd0(X1,qtd1)))) = qtd1,
inference(hyper_resolution,[status(thm)],[hi5,h11,h36]) ).
cnf(t14359,plain,
qtd3(X1,qtd3(X2,qtd0(X2,X1))) = qtd1,
inference(step,[status(thm)],[t55,t256]) ).
cnf(h489,plain,
qtd2(qtd3(V0,V1),qtd3(V2,qtd3(V3,qtd0(V3,qtd0(V2,qtd1))))) = true,
inference(hyper_resolution,[status(thm)],[hi4,h11,h36]) ).
cnf(h66,plain,
qtd2(qtd3(V0,qtd3(V1,V2)),qtd3(V0,qtd1)) = true,
inference(hyper_resolution,[status(thm)],[hi11,h11]) ).
cnf(t127,plain,
qtd3(X1,qtd3(X2,qtd0(X2,qtd0(X1,qtd1)))) = qtd3(X1,qtd1),
inference(hyper_resolution,[status(thm)],[hi5,h66,h489]) ).
cnf(t14358,plain,
qtd3(X1,qtd3(X2,qtd0(X2,X1))) = qtd3(X1,qtd1),
inference(step,[status(thm)],[t127,t256]) ).
cnf(t272,plain,
qtd3(X1,qtd3(X2,qtd0(X2,X1))) = qtd3(X1,qtd1),
inference(orient,[status(thm)],[t14358]) ).
cnf(t14360,plain,
qtd3(X1,qtd1) = qtd1,
inference(step,[status(thm)],[t14359,t272]) ).
cnf(t274,plain,
qtd3(X1,qtd1) = qtd1,
inference(orient,[status(thm)],[t14360]) ).
cnf(t14387,plain,
true = qtd2(X1,qtd3(qtd0(X2,qtd1),X1)),
inference(step,[status(thm)],[t908,t274]) ).
cnf(t14388,plain,
true = qtd2(X1,qtd3(X2,X1)),
inference(step,[status(thm)],[t14387,t256]) ).
cnf(t1060,plain,
qtd2(X1,qtd3(X2,X1)) = true,
inference(orient,[status(thm)],[t14388]) ).
cnf(t14393,plain,
X1 = ifeq(true,true,qtd3(qtd3(X1,qtd4),X1),X1),
inference(step,[status(thm)],[t14392,t1060]) ).
cnf(t14394,plain,
X1 = qtd3(qtd3(X1,qtd4),X1),
inference(step,[status(thm)],[t14393,t257]) ).
cnf(t1130,plain,
qtd3(qtd3(X1,qtd4),X1) = X1,
inference(orient,[status(thm)],[t14394]) ).
cnf(t1146,plain,
true = qtd2(qtd3(qtd3(X1,qtd0(X1,qtd3(X2,qtd4))),X2),X2),
inference(cp,[status(thm)],[t517,t1130]) ).
cnf(t14120,plain,
qtd2(qtd3(qtd3(X1,qtd0(X1,qtd3(X2,qtd4))),X2),X2) = true,
inference(orient,[status(thm)],[t1146]) ).
fof(f11,axiom,
! [A] : qtd0(A,qtd4) = qtd4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_12) ).
fof(f11_nnf,plain,
! [A] : qtd0(A,qtd4) = qtd4,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A] : qtd0(A,qtd4) = qtd4,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c12,plain,
qtd0(X0,qtd4) = qtd4,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t1,plain,
qtd0(X1,qtd4) = qtd4,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t392,plain,
qtd0(X1,qtd4) = qtd4,
inference(orient,[status(thm)],[t1]) ).
cnf(t393,plain,
qtd4 = qtd0(qtd4,X1),
inference(cp,[status(thm)],[t392,t368]) ).
cnf(t922,plain,
qtd0(qtd4,X1) = qtd4,
inference(orient,[status(thm)],[t393]) ).
cnf(t928,plain,
true = qtd2(qtd4,X1),
inference(cp,[status(thm)],[t556,t922]) ).
cnf(t1001,plain,
qtd2(qtd4,X1) = true,
inference(orient,[status(thm)],[t928]) ).
cnf(t1002,plain,
X1 = ifeq(true,true,ifeq(qtd2(X1,qtd4),true,qtd4,X1),X1),
inference(cp,[status(thm)],[t258,t1001]) ).
cnf(t14396,plain,
X1 = ifeq(qtd2(X1,qtd4),true,qtd4,X1),
inference(step,[status(thm)],[t1002,t257]) ).
cnf(t1176,plain,
ifeq(qtd2(X1,qtd4),true,qtd4,X1) = X1,
inference(orient,[status(thm)],[t14396]) ).
cnf(t101,plain,
qtd2(qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,X3)))),X3) = true,
inference(hyper_resolution,[status(thm)],[hi7,h2]) ).
cnf(t611,plain,
qtd2(qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,X3)))),X3) = true,
inference(orient,[status(thm)],[t101]) ).
cnf(t1178,plain,
qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4)))) = ifeq(true,true,qtd4,qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4))))),
inference(cp,[status(thm)],[t1176,t611]) ).
cnf(t14437,plain,
qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4)))) = qtd4,
inference(step,[status(thm)],[t1178,t257]) ).
cnf(t2155,plain,
qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4)))) = qtd4,
inference(orient,[status(thm)],[t14437]) ).
cnf(t118,plain,
qtd2(qtd3(X1,qtd0(X2,qtd3(X2,X3))),qtd3(X1,X3)) = true,
inference(hyper_resolution,[status(thm)],[hi11,h2]) ).
cnf(t506,plain,
qtd2(qtd3(X1,qtd0(X2,qtd3(X2,X3))),qtd3(X1,X3)) = true,
inference(orient,[status(thm)],[t118]) ).
cnf(t940,plain,
true = qtd2(qtd3(X1,qtd4),qtd3(X1,X2)),
inference(cp,[status(thm)],[t506,t922]) ).
cnf(t1167,plain,
qtd2(qtd3(X1,qtd4),qtd3(X1,X2)) = true,
inference(orient,[status(thm)],[t940]) ).
cnf(t1168,plain,
true = qtd2(qtd3(qtd3(X1,qtd4),qtd4),X1),
inference(cp,[status(thm)],[t1167,t1130]) ).
cnf(t1273,plain,
qtd2(qtd3(qtd3(X1,qtd4),qtd4),X1) = true,
inference(orient,[status(thm)],[t1168]) ).
cnf(t1274,plain,
X1 = ifeq(true,true,ifeq(qtd2(X1,qtd3(qtd3(X1,qtd4),qtd4)),true,qtd3(qtd3(X1,qtd4),qtd4),X1),X1),
inference(cp,[status(thm)],[t258,t1273]) ).
cnf(t14400,plain,
X1 = ifeq(qtd2(X1,qtd3(qtd3(X1,qtd4),qtd4)),true,qtd3(qtd3(X1,qtd4),qtd4),X1),
inference(step,[status(thm)],[t1274,t257]) ).
cnf(t13,plain,
qtd2(X1,qtd3(X2,qtd0(X2,X1))) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi3]) ).
cnf(t432,plain,
qtd2(X1,qtd3(X2,qtd0(X2,X1))) = true,
inference(orient,[status(thm)],[t13]) ).
cnf(t436,plain,
true = qtd2(X1,qtd3(X2,qtd0(X1,X2))),
inference(cp,[status(thm)],[t432,t368]) ).
cnf(t1099,plain,
qtd2(X1,qtd3(X2,qtd0(X1,X2))) = true,
inference(orient,[status(thm)],[t436]) ).
cnf(t395,plain,
qtd0(X1,qtd4) = qtd0(X1,qtd3(X1,qtd4)),
inference(cp,[status(thm)],[t376,t392]) ).
cnf(t14382,plain,
qtd4 = qtd0(X1,qtd3(X1,qtd4)),
inference(step,[status(thm)],[t395,t392]) ).
cnf(t1022,plain,
qtd0(X1,qtd3(X1,qtd4)) = qtd4,
inference(orient,[status(thm)],[t14382]) ).
cnf(t1102,plain,
true = qtd2(X1,qtd3(qtd3(X1,qtd4),qtd4)),
inference(cp,[status(thm)],[t1099,t1022]) ).
cnf(t1263,plain,
qtd2(X1,qtd3(qtd3(X1,qtd4),qtd4)) = true,
inference(orient,[status(thm)],[t1102]) ).
cnf(t14401,plain,
X1 = ifeq(true,true,qtd3(qtd3(X1,qtd4),qtd4),X1),
inference(step,[status(thm)],[t14400,t1263]) ).
cnf(t14402,plain,
X1 = qtd3(qtd3(X1,qtd4),qtd4),
inference(step,[status(thm)],[t14401,t257]) ).
cnf(t1282,plain,
qtd3(qtd3(X1,qtd4),qtd4) = X1,
inference(orient,[status(thm)],[t14402]) ).
cnf(t2160,plain,
qtd4 = qtd0(qtd3(X1,qtd4),qtd0(X2,qtd3(X2,X1))),
inference(cp,[status(thm)],[t2155,t1282]) ).
cnf(t4156,plain,
qtd0(qtd3(X1,qtd4),qtd0(X2,qtd3(X2,X1))) = qtd4,
inference(orient,[status(thm)],[t2160]) ).
cnf(t3,plain,
qtd2(X1,qtd1) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t473,plain,
qtd2(X1,qtd1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t475,plain,
X1 = ifeq(qtd2(qtd1,X1),true,ifeq(true,true,qtd1,X1),X1),
inference(cp,[status(thm)],[t258,t473]) ).
cnf(t14390,plain,
X1 = ifeq(qtd2(qtd1,X1),true,qtd1,X1),
inference(step,[status(thm)],[t475,t257]) ).
cnf(t1118,plain,
ifeq(qtd2(qtd1,X1),true,qtd1,X1) = X1,
inference(orient,[status(thm)],[t14390]) ).
cnf(t141,plain,
ifeq(qtd2(qtd0(X1,X2),X3),true,qtd2(X2,qtd3(X1,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t858,plain,
ifeq(qtd2(qtd0(X1,X2),X3),true,qtd2(X2,qtd3(X1,X3)),true) = true,
inference(orient,[status(thm)],[t141]) ).
fof(f0,axiom,
! [A,B,C] : qtd0(qtd0(A,B),C) = qtd0(A,qtd0(B,C)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_01) ).
fof(f0_nnf,plain,
! [A,B,C] : qtd0(qtd0(A,B),C) = qtd0(A,qtd0(B,C)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B,C] : qtd0(qtd0(A,B),C) = qtd0(A,qtd0(B,C)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
qtd0(qtd0(X0,X1),X2) = qtd0(X0,qtd0(X1,X2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t36,plain,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t379,plain,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
inference(orient,[status(thm)],[t36]) ).
cnf(t1024,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd0(qtd4,X2),
inference(cp,[status(thm)],[t379,t1022]) ).
cnf(t14398,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd4,
inference(step,[status(thm)],[t1024,t922]) ).
cnf(t1184,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd4,
inference(orient,[status(thm)],[t14398]) ).
cnf(t1189,plain,
true = ifeq(qtd2(qtd4,X1),true,qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),true),
inference(cp,[status(thm)],[t858,t1184]) ).
cnf(t14439,plain,
true = ifeq(true,true,qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),true),
inference(step,[status(thm)],[t1189,t1001]) ).
cnf(t14440,plain,
true = qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),
inference(step,[status(thm)],[t14439,t257]) ).
cnf(t2264,plain,
qtd2(qtd0(qtd3(X1,qtd4),X2),qtd3(X1,X3)) = true,
inference(orient,[status(thm)],[t14440]) ).
cnf(t2269,plain,
true = ifeq(true,true,qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))),true),
inference(cp,[status(thm)],[t858,t2264]) ).
cnf(t14491,plain,
true = qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))),
inference(step,[status(thm)],[t2269,t257]) ).
cnf(t4208,plain,
qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))) = true,
inference(orient,[status(thm)],[t14491]) ).
cnf(t4211,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = ifeq(true,true,qtd1,qtd3(qtd3(X1,qtd4),qtd3(X1,X2))),
inference(cp,[status(thm)],[t1118,t4208]) ).
cnf(t14492,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = qtd1,
inference(step,[status(thm)],[t4211,t257]) ).
cnf(t4220,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = qtd1,
inference(orient,[status(thm)],[t14492]) ).
cnf(t4223,plain,
qtd4 = qtd0(qtd3(qtd3(X1,X2),qtd4),qtd0(qtd3(X1,qtd4),qtd1)),
inference(cp,[status(thm)],[t4156,t4220]) ).
cnf(t14509,plain,
qtd4 = qtd0(qtd3(qtd3(X1,X2),qtd4),qtd3(X1,qtd4)),
inference(step,[status(thm)],[t4223,t256]) ).
cnf(t14510,plain,
qtd4 = qtd0(qtd3(X1,qtd4),qtd3(qtd3(X1,X2),qtd4)),
inference(step,[status(thm)],[t14509,t368]) ).
cnf(t5238,plain,
qtd0(qtd3(X1,qtd4),qtd3(qtd3(X1,X2),qtd4)) = qtd4,
inference(orient,[status(thm)],[t14510]) ).
cnf(t14127,plain,
true = qtd2(qtd3(qtd3(qtd3(X1,qtd4),qtd4),qtd3(X1,X2)),qtd3(X1,X2)),
inference(cp,[status(thm)],[t14120,t5238]) ).
cnf(t14594,plain,
true = qtd2(qtd3(X1,qtd3(X1,X2)),qtd3(X1,X2)),
inference(step,[status(thm)],[t14127,t1282]) ).
cnf(t14146,plain,
qtd2(qtd3(X1,qtd3(X1,X2)),qtd3(X1,X2)) = true,
inference(orient,[status(thm)],[t14594]) ).
cnf(t14164,plain,
qtd3(X1,X2) = ifeq(true,true,ifeq(qtd2(qtd3(X1,X2),qtd3(X1,qtd3(X1,X2))),true,qtd3(X1,qtd3(X1,X2)),qtd3(X1,X2)),qtd3(X1,X2)),
inference(cp,[status(thm)],[t258,t14146]) ).
cnf(t14595,plain,
qtd3(X1,X2) = ifeq(qtd2(qtd3(X1,X2),qtd3(X1,qtd3(X1,X2))),true,qtd3(X1,qtd3(X1,X2)),qtd3(X1,X2)),
inference(step,[status(thm)],[t14164,t257]) ).
cnf(t139,plain,
ifeq(qtd2(X1,X2),true,qtd2(qtd3(X3,X1),qtd3(X3,X2)),true) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t662,plain,
ifeq(qtd2(X1,X2),true,qtd2(qtd3(X3,X1),qtd3(X3,X2)),true) = true,
inference(orient,[status(thm)],[t139]) ).
cnf(t1070,plain,
true = ifeq(true,true,qtd2(qtd3(X1,X2),qtd3(X1,qtd3(X3,X2))),true),
inference(cp,[status(thm)],[t662,t1060]) ).
cnf(t14432,plain,
true = qtd2(qtd3(X1,X2),qtd3(X1,qtd3(X3,X2))),
inference(step,[status(thm)],[t1070,t257]) ).
cnf(t2025,plain,
qtd2(qtd3(X1,X2),qtd3(X1,qtd3(X3,X2))) = true,
inference(orient,[status(thm)],[t14432]) ).
cnf(t14596,plain,
qtd3(X1,X2) = ifeq(true,true,qtd3(X1,qtd3(X1,X2)),qtd3(X1,X2)),
inference(step,[status(thm)],[t14595,t2025]) ).
cnf(t14597,plain,
qtd3(X1,X2) = qtd3(X1,qtd3(X1,X2)),
inference(step,[status(thm)],[t14596,t257]) ).
cnf(t14177,plain,
qtd3(X1,qtd3(X1,X2)) = qtd3(X1,X2),
inference(orient,[status(thm)],[t14597]) ).
cnf(t14363,plain,
qtd3(X1,qtd3(X2,qtd0(X2,X1))) = qtd1,
inference(step,[status(thm)],[t272,t274]) ).
cnf(t277,plain,
qtd3(X1,qtd3(X2,qtd0(X2,X1))) = qtd1,
inference(orient,[status(thm)],[t14363]) ).
cnf(t14180,plain,
qtd3(X1,qtd0(X1,X1)) = qtd1,
inference(cp,[status(thm)],[t14177,t277]) ).
cnf(t14220,plain,
qtd3(X1,qtd0(X1,X1)) = qtd1,
inference(orient,[status(thm)],[t14180]) ).
cnf(t14247,plain,
qtd0(X1,X1) = qtd0(X1,qtd1),
inference(cp,[status(thm)],[t1595,t14220]) ).
cnf(t14598,plain,
qtd0(X1,X1) = X1,
inference(step,[status(thm)],[t14247,t256]) ).
cnf(t14295,plain,
qtd0(X1,X1) = X1,
inference(orient,[status(thm)],[t14598]) ).
fof(f13,conjecture,
! [X17] : qtd0(X17,X17) = X17,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f13_neg,negated_conjecture,
~ ! [X17] : qtd0(X17,X17) = X17,
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X17] : qtd0(X17,X17) != X17,
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
qtd0(sk0,sk0) != sk0,
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f13_nnf]) ).
cnf(c14,plain,
qtd0(sk0,sk0) != sk0,
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
qtd0(sk0,sk0) != sk0,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(g0_0,plain,
sk0 != sk0,
inference(rw,[status(thm)],[goal_0,t14295]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL903+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.35 % Computer : n002.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Thu Sep 24 00:42:33 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 43.02/5.88 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 43.02/5.88 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------