%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL900+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 : n005.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 82.84s 10.98s
% Output : Proof 82.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 15
% Syntax : Number of formulae : 265 ( 240 unt; 0 def)
% Number of atoms : 302 ( 235 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 : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-4 aty)
% Number of variables : 553 ( 66 sgn 88 !; 2 ?)
% 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(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]) ).
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(h2,plain,
qtd2(qtd0(V0,qtd3(V0,V1)),V1) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3]) ).
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(h24,plain,
qtd2(qtd3(V0,qtd0(V1,qtd3(V1,V2))),qtd3(V0,V2)) = true,
inference(hyper_resolution,[status(thm)],[hi11,h2]) ).
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]) ).
cnf(h3,plain,
qtd2(V0,qtd3(V1,qtd0(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi3]) ).
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(t57,plain,
qtd3(X1,qtd0(X1,qtd3(X1,X2))) = qtd3(X1,X2),
inference(hyper_resolution,[status(thm)],[hi5,h3,h24]) ).
cnf(t259,plain,
qtd3(X1,qtd0(X1,qtd3(X1,X2))) = qtd3(X1,X2),
inference(orient,[status(thm)],[t57]) ).
fof(f12,axiom,
! [A,B] : qtd3(qtd3(A,B),B) = qtd3(qtd3(B,A),A),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',sos_13) ).
fof(f12_nnf,plain,
! [A,B] : qtd3(qtd3(A,B),B) = qtd3(qtd3(B,A),A),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] : qtd3(qtd3(A,B),B) = qtd3(qtd3(B,A),A),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
qtd3(qtd3(X0,X1),X1) = qtd3(qtd3(X1,X0),X0),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t89,plain,
qtd3(qtd3(X1,X2),X2) = qtd3(qtd3(X2,X1),X1),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t282,plain,
qtd3(qtd3(X1,X2),X2) = qtd3(qtd3(X2,X1),X1),
inference(orient,[status(thm)],[t89]) ).
cnf(t287,plain,
qtd3(qtd3(X1,X2),X2) = qtd3(qtd3(X1,X2),qtd0(qtd3(X1,X2),qtd3(qtd3(X2,X1),X1))),
inference(cp,[status(thm)],[t259,t282]) ).
cnf(t2818,plain,
qtd3(qtd3(X1,X2),qtd0(qtd3(X1,X2),qtd3(qtd3(X2,X1),X1))) = qtd3(qtd3(X1,X2),X2),
inference(orient,[status(thm)],[t287]) ).
cnf(t168,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)],[t168]) ).
cnf(t112,plain,
qtd2(X1,qtd3(X2,qtd3(X3,qtd0(X3,qtd0(X2,X1))))) = true,
inference(hyper_resolution,[status(thm)],[hi6,h3]) ).
cnf(t305,plain,
qtd2(X1,qtd3(X2,qtd3(X3,qtd0(X3,qtd0(X2,X1))))) = true,
inference(orient,[status(thm)],[t112]) ).
cnf(t22,plain,
qtd2(qtd0(X1,qtd3(X1,X2)),X2) = true,
inference(hyper_resolution,[status(thm)],[hi7,hi3]) ).
cnf(t407,plain,
qtd2(qtd0(X1,qtd3(X1,X2)),X2) = true,
inference(orient,[status(thm)],[t22]) ).
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(t300,plain,
qtd0(X1,qtd4) = qtd4,
inference(orient,[status(thm)],[t1]) ).
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(t290,plain,
qtd0(X1,X2) = qtd0(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t301,plain,
qtd4 = qtd0(qtd4,X1),
inference(cp,[status(thm)],[t300,t290]) ).
cnf(t711,plain,
qtd0(qtd4,X1) = qtd4,
inference(orient,[status(thm)],[t301]) ).
cnf(t717,plain,
true = qtd2(qtd4,X1),
inference(cp,[status(thm)],[t407,t711]) ).
cnf(t738,plain,
qtd2(qtd4,X1) = true,
inference(orient,[status(thm)],[t717]) ).
cnf(t739,plain,
X1 = ifeq(true,true,ifeq(qtd2(X1,qtd4),true,qtd4,X1),X1),
inference(cp,[status(thm)],[t258,t738]) ).
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(t90631,plain,
X1 = ifeq(qtd2(X1,qtd4),true,qtd4,X1),
inference(step,[status(thm)],[t739,t257]) ).
cnf(t1008,plain,
ifeq(qtd2(X1,qtd4),true,qtd4,X1) = X1,
inference(orient,[status(thm)],[t90631]) ).
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(h25,plain,
qtd2(qtd3(V0,V1),qtd3(qtd0(V2,qtd3(V2,V0)),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi10,h2]) ).
cnf(t131,plain,
qtd2(qtd0(qtd0(X1,qtd3(X1,X2)),qtd3(X2,X3)),X3) = true,
inference(hyper_resolution,[status(thm)],[hi7,h25]) ).
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(t50,plain,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t293,plain,
qtd0(qtd0(X1,X2),X3) = qtd0(X1,qtd0(X2,X3)),
inference(orient,[status(thm)],[t50]) ).
cnf(t90616,plain,
qtd2(qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,X3))),X3) = true,
inference(step,[status(thm)],[t131,t293]) ).
cnf(t469,plain,
qtd2(qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,X3))),X3) = true,
inference(orient,[status(thm)],[t90616]) ).
cnf(t1009,plain,
qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,qtd4))) = ifeq(true,true,qtd4,qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,qtd4)))),
inference(cp,[status(thm)],[t1008,t469]) ).
cnf(t90670,plain,
qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,qtd4))) = qtd4,
inference(step,[status(thm)],[t1009,t257]) ).
cnf(t1743,plain,
qtd0(X1,qtd0(qtd3(X1,X2),qtd3(X2,qtd4))) = qtd4,
inference(orient,[status(thm)],[t90670]) ).
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(h241,plain,
qtd2(V0,qtd3(qtd0(V1,qtd3(V1,V2)),qtd0(V2,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi4,h3,h25]) ).
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]) ).
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(h21,plain,
qtd2(qtd3(qtd0(V0,V1),V2),qtd3(qtd0(V0,V1),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi10,h1]) ).
cnf(h187,plain,
qtd2(qtd3(qtd0(V0,V1),V2),qtd1) = true,
inference(hyper_resolution,[status(thm)],[hi4,h21,h11]) ).
cnf(t73,plain,
qtd3(qtd0(X1,qtd3(X1,X2)),qtd0(X2,qtd1)) = qtd1,
inference(hyper_resolution,[status(thm)],[hi5,h187,h241]) ).
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(t90614,plain,
qtd3(qtd0(X1,qtd3(X1,X2)),X2) = qtd1,
inference(step,[status(thm)],[t73,t256]) ).
cnf(t288,plain,
qtd3(qtd0(X1,qtd3(X1,X2)),X2) = qtd1,
inference(orient,[status(thm)],[t90614]) ).
cnf(t718,plain,
qtd1 = qtd3(qtd4,X1),
inference(cp,[status(thm)],[t288,t711]) ).
cnf(t746,plain,
qtd3(qtd4,X1) = qtd1,
inference(orient,[status(thm)],[t718]) ).
cnf(t759,plain,
qtd3(qtd3(X1,qtd4),qtd4) = qtd3(qtd1,X1),
inference(cp,[status(thm)],[t282,t746]) ).
cnf(t20,plain,
qtd2(X1,qtd3(X2,qtd0(X2,X1))) = true,
inference(hyper_resolution,[status(thm)],[hi6,hi3]) ).
cnf(t313,plain,
qtd2(X1,qtd3(X2,qtd0(X2,X1))) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t291,plain,
qtd0(qtd1,X1) = X1,
inference(cp,[status(thm)],[t290,t256]) ).
cnf(t676,plain,
qtd0(qtd1,X1) = X1,
inference(orient,[status(thm)],[t291]) ).
cnf(t684,plain,
true = qtd2(X1,qtd3(qtd1,X1)),
inference(cp,[status(thm)],[t313,t676]) ).
cnf(t820,plain,
qtd2(X1,qtd3(qtd1,X1)) = true,
inference(orient,[status(thm)],[t684]) ).
cnf(t821,plain,
qtd3(qtd1,X1) = ifeq(true,true,ifeq(qtd2(qtd3(qtd1,X1),X1),true,X1,qtd3(qtd1,X1)),qtd3(qtd1,X1)),
inference(cp,[status(thm)],[t258,t820]) ).
cnf(t90621,plain,
qtd3(qtd1,X1) = ifeq(qtd2(qtd3(qtd1,X1),X1),true,X1,qtd3(qtd1,X1)),
inference(step,[status(thm)],[t821,t257]) ).
cnf(t683,plain,
true = qtd2(qtd3(qtd1,X1),X1),
inference(cp,[status(thm)],[t407,t676]) ).
cnf(t809,plain,
qtd2(qtd3(qtd1,X1),X1) = true,
inference(orient,[status(thm)],[t683]) ).
cnf(t90622,plain,
qtd3(qtd1,X1) = ifeq(true,true,X1,qtd3(qtd1,X1)),
inference(step,[status(thm)],[t90621,t809]) ).
cnf(t90623,plain,
qtd3(qtd1,X1) = X1,
inference(step,[status(thm)],[t90622,t257]) ).
cnf(t895,plain,
qtd3(qtd1,X1) = X1,
inference(orient,[status(thm)],[t90623]) ).
cnf(t90626,plain,
qtd3(qtd3(X1,qtd4),qtd4) = X1,
inference(step,[status(thm)],[t759,t895]) ).
cnf(t917,plain,
qtd3(qtd3(X1,qtd4),qtd4) = X1,
inference(orient,[status(thm)],[t90626]) ).
cnf(t1754,plain,
qtd4 = qtd0(X1,qtd0(qtd3(X1,qtd3(X2,qtd4)),X2)),
inference(cp,[status(thm)],[t1743,t917]) ).
cnf(t90707,plain,
qtd4 = qtd0(X1,qtd0(X2,qtd3(X1,qtd3(X2,qtd4)))),
inference(step,[status(thm)],[t1754,t290]) ).
cnf(t3291,plain,
qtd0(X1,qtd0(X2,qtd3(X1,qtd3(X2,qtd4)))) = qtd4,
inference(orient,[status(thm)],[t90707]) ).
cnf(t3337,plain,
true = qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(X2,qtd3(X1,qtd4))),
inference(cp,[status(thm)],[t305,t3291]) ).
cnf(t24907,plain,
qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(X2,qtd3(X1,qtd4))) = true,
inference(orient,[status(thm)],[t3337]) ).
cnf(t24940,plain,
qtd3(X1,qtd3(X2,qtd4)) = ifeq(true,true,ifeq(qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(X2,qtd3(X1,qtd4))),true,qtd3(X2,qtd3(X1,qtd4)),qtd3(X1,qtd3(X2,qtd4))),qtd3(X1,qtd3(X2,qtd4))),
inference(cp,[status(thm)],[t258,t24907]) ).
cnf(t90978,plain,
qtd3(X1,qtd3(X2,qtd4)) = ifeq(qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(X2,qtd3(X1,qtd4))),true,qtd3(X2,qtd3(X1,qtd4)),qtd3(X1,qtd3(X2,qtd4))),
inference(step,[status(thm)],[t24940,t257]) ).
cnf(t90979,plain,
qtd3(X1,qtd3(X2,qtd4)) = ifeq(true,true,qtd3(X2,qtd3(X1,qtd4)),qtd3(X1,qtd3(X2,qtd4))),
inference(step,[status(thm)],[t90978,t24907]) ).
cnf(t90980,plain,
qtd3(X1,qtd3(X2,qtd4)) = qtd3(X2,qtd3(X1,qtd4)),
inference(step,[status(thm)],[t90979,t257]) ).
cnf(t24951,plain,
qtd3(X1,qtd3(X2,qtd4)) = qtd3(X2,qtd3(X1,qtd4)),
inference(orient,[status(thm)],[t90980]) ).
cnf(t3,plain,
qtd2(X1,qtd1) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t344,plain,
qtd2(X1,qtd1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t346,plain,
X1 = ifeq(qtd2(qtd1,X1),true,ifeq(true,true,qtd1,X1),X1),
inference(cp,[status(thm)],[t258,t344]) ).
cnf(t90629,plain,
X1 = ifeq(qtd2(qtd1,X1),true,qtd1,X1),
inference(step,[status(thm)],[t346,t257]) ).
cnf(t993,plain,
ifeq(qtd2(qtd1,X1),true,qtd1,X1) = X1,
inference(orient,[status(thm)],[t90629]) ).
cnf(t173,plain,
ifeq(qtd2(qtd0(X1,X2),X3),true,qtd2(X2,qtd3(X1,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t656,plain,
ifeq(qtd2(qtd0(X1,X2),X3),true,qtd2(X2,qtd3(X1,X3)),true) = true,
inference(orient,[status(thm)],[t173]) ).
cnf(t918,plain,
qtd0(X1,qtd3(X1,qtd4)) = qtd3(qtd1,qtd4),
inference(cp,[status(thm)],[t917,t288]) ).
cnf(t90627,plain,
qtd0(X1,qtd3(X1,qtd4)) = qtd4,
inference(step,[status(thm)],[t918,t895]) ).
cnf(t943,plain,
qtd0(X1,qtd3(X1,qtd4)) = qtd4,
inference(orient,[status(thm)],[t90627]) ).
cnf(t947,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd0(qtd4,X2),
inference(cp,[status(thm)],[t293,t943]) ).
cnf(t90635,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd4,
inference(step,[status(thm)],[t947,t711]) ).
cnf(t1052,plain,
qtd0(X1,qtd0(qtd3(X1,qtd4),X2)) = qtd4,
inference(orient,[status(thm)],[t90635]) ).
cnf(t1059,plain,
true = ifeq(qtd2(qtd4,X1),true,qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),true),
inference(cp,[status(thm)],[t656,t1052]) ).
cnf(t90674,plain,
true = ifeq(true,true,qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),true),
inference(step,[status(thm)],[t1059,t738]) ).
cnf(t90675,plain,
true = qtd2(qtd0(qtd3(X2,qtd4),X3),qtd3(X2,X1)),
inference(step,[status(thm)],[t90674,t257]) ).
cnf(t1930,plain,
qtd2(qtd0(qtd3(X1,qtd4),X2),qtd3(X1,X3)) = true,
inference(orient,[status(thm)],[t90675]) ).
cnf(t1940,plain,
true = ifeq(true,true,qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))),true),
inference(cp,[status(thm)],[t656,t1930]) ).
cnf(t90713,plain,
true = qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))),
inference(step,[status(thm)],[t1940,t257]) ).
cnf(t3545,plain,
qtd2(X1,qtd3(qtd3(X2,qtd4),qtd3(X2,X3))) = true,
inference(orient,[status(thm)],[t90713]) ).
cnf(t3553,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = ifeq(true,true,qtd1,qtd3(qtd3(X1,qtd4),qtd3(X1,X2))),
inference(cp,[status(thm)],[t993,t3545]) ).
cnf(t90714,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = qtd1,
inference(step,[status(thm)],[t3553,t257]) ).
cnf(t3562,plain,
qtd3(qtd3(X1,qtd4),qtd3(X1,X2)) = qtd1,
inference(orient,[status(thm)],[t90714]) ).
cnf(t3563,plain,
qtd1 = qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),
inference(cp,[status(thm)],[t3562,t917]) ).
cnf(t3597,plain,
qtd3(X1,qtd3(qtd3(X1,qtd4),X2)) = qtd1,
inference(orient,[status(thm)],[t3563]) ).
cnf(t3612,plain,
qtd3(qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),qtd3(qtd3(X1,qtd4),X2)) = qtd3(qtd1,qtd0(qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1))),
inference(cp,[status(thm)],[t2818,t3597]) ).
cnf(t90772,plain,
qtd3(qtd1,qtd3(qtd3(X1,qtd4),X2)) = qtd3(qtd1,qtd0(qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1))),
inference(step,[status(thm)],[t3612,t3597]) ).
cnf(t90773,plain,
qtd3(qtd3(X1,qtd4),X2) = qtd3(qtd1,qtd0(qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1))),
inference(step,[status(thm)],[t90772,t895]) ).
cnf(t90774,plain,
qtd3(qtd3(X1,qtd4),X2) = qtd0(qtd3(X1,qtd3(qtd3(X1,qtd4),X2)),qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1)),
inference(step,[status(thm)],[t90773,t895]) ).
cnf(t90775,plain,
qtd3(qtd3(X1,qtd4),X2) = qtd0(qtd1,qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1)),
inference(step,[status(thm)],[t90774,t3597]) ).
cnf(t90776,plain,
qtd3(qtd3(X1,qtd4),X2) = qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1),
inference(step,[status(thm)],[t90775,t676]) ).
cnf(t7723,plain,
qtd3(qtd3(qtd3(qtd3(X1,qtd4),X2),X1),X1) = qtd3(qtd3(X1,qtd4),X2),
inference(orient,[status(thm)],[t90776]) ).
cnf(t24972,plain,
qtd3(qtd3(qtd3(qtd3(qtd4,qtd4),X1),qtd4),qtd3(X2,qtd4)) = qtd3(X2,qtd3(qtd3(qtd4,qtd4),X1)),
inference(cp,[status(thm)],[t24951,t7723]) ).
cnf(t90981,plain,
qtd3(qtd3(qtd3(qtd1,X1),qtd4),qtd3(X2,qtd4)) = qtd3(X2,qtd3(qtd3(qtd4,qtd4),X1)),
inference(step,[status(thm)],[t24972,t746]) ).
cnf(t90982,plain,
qtd3(qtd3(X1,qtd4),qtd3(X2,qtd4)) = qtd3(X2,qtd3(qtd3(qtd4,qtd4),X1)),
inference(step,[status(thm)],[t90981,t895]) ).
cnf(t90983,plain,
qtd3(qtd3(X1,qtd4),qtd3(X2,qtd4)) = qtd3(X2,qtd3(qtd1,X1)),
inference(step,[status(thm)],[t90982,t746]) ).
cnf(t90984,plain,
qtd3(qtd3(X1,qtd4),qtd3(X2,qtd4)) = qtd3(X2,X1),
inference(step,[status(thm)],[t90983,t895]) ).
cnf(t25291,plain,
qtd3(qtd3(X1,qtd4),qtd3(X2,qtd4)) = qtd3(X2,X1),
inference(orient,[status(thm)],[t90984]) ).
cnf(t315,plain,
true = qtd2(X1,qtd3(qtd0(X2,X3),qtd0(X2,qtd0(X3,X1)))),
inference(cp,[status(thm)],[t313,t293]) ).
cnf(t8109,plain,
qtd2(X1,qtd3(qtd0(X2,X3),qtd0(X2,qtd0(X3,X1)))) = true,
inference(orient,[status(thm)],[t315]) ).
cnf(t121,plain,
qtd2(qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,X3)))),X3) = true,
inference(hyper_resolution,[status(thm)],[hi7,h2]) ).
cnf(t447,plain,
qtd2(qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,X3)))),X3) = true,
inference(orient,[status(thm)],[t121]) ).
cnf(t1010,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)],[t1008,t447]) ).
cnf(t90672,plain,
qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4)))) = qtd4,
inference(step,[status(thm)],[t1010,t257]) ).
cnf(t1815,plain,
qtd0(X1,qtd0(X2,qtd3(X2,qtd3(X1,qtd4)))) = qtd4,
inference(orient,[status(thm)],[t90672]) ).
cnf(t8119,plain,
true = qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(qtd0(X2,X1),qtd4)),
inference(cp,[status(thm)],[t8109,t1815]) ).
cnf(t76314,plain,
qtd2(qtd3(X1,qtd3(X2,qtd4)),qtd3(qtd0(X2,X1),qtd4)) = true,
inference(orient,[status(thm)],[t8119]) ).
cnf(t76388,plain,
qtd3(qtd0(X1,X2),qtd4) = ifeq(true,true,ifeq(qtd2(qtd3(qtd0(X1,X2),qtd4),qtd3(X2,qtd3(X1,qtd4))),true,qtd3(X2,qtd3(X1,qtd4)),qtd3(qtd0(X1,X2),qtd4)),qtd3(qtd0(X1,X2),qtd4)),
inference(cp,[status(thm)],[t258,t76314]) ).
cnf(t91309,plain,
qtd3(qtd0(X1,X2),qtd4) = ifeq(qtd2(qtd3(qtd0(X1,X2),qtd4),qtd3(X2,qtd3(X1,qtd4))),true,qtd3(X2,qtd3(X1,qtd4)),qtd3(qtd0(X1,X2),qtd4)),
inference(step,[status(thm)],[t76388,t257]) ).
cnf(t944,plain,
qtd4 = qtd0(X1,qtd0(X2,qtd3(qtd0(X1,X2),qtd4))),
inference(cp,[status(thm)],[t943,t293]) ).
cnf(t1643,plain,
qtd0(X1,qtd0(X2,qtd3(qtd0(X1,X2),qtd4))) = qtd4,
inference(orient,[status(thm)],[t944]) ).
cnf(t1670,plain,
true = qtd2(qtd3(qtd0(X1,X2),qtd4),qtd3(X2,qtd3(X1,qtd4))),
inference(cp,[status(thm)],[t305,t1643]) ).
cnf(t15946,plain,
qtd2(qtd3(qtd0(X1,X2),qtd4),qtd3(X2,qtd3(X1,qtd4))) = true,
inference(orient,[status(thm)],[t1670]) ).
cnf(t91310,plain,
qtd3(qtd0(X1,X2),qtd4) = ifeq(true,true,qtd3(X2,qtd3(X1,qtd4)),qtd3(qtd0(X1,X2),qtd4)),
inference(step,[status(thm)],[t91309,t15946]) ).
cnf(t91311,plain,
qtd3(qtd0(X1,X2),qtd4) = qtd3(X2,qtd3(X1,qtd4)),
inference(step,[status(thm)],[t91310,t257]) ).
cnf(t76399,plain,
qtd3(qtd0(X1,X2),qtd4) = qtd3(X2,qtd3(X1,qtd4)),
inference(orient,[status(thm)],[t91311]) ).
cnf(t76429,plain,
qtd3(X1,qtd3(qtd0(X2,X3),qtd4)) = qtd3(qtd0(X2,qtd0(X3,X1)),qtd4),
inference(cp,[status(thm)],[t76399,t293]) ).
cnf(t91385,plain,
qtd3(X1,qtd3(X3,qtd3(X2,qtd4))) = qtd3(qtd0(X2,qtd0(X3,X1)),qtd4),
inference(step,[status(thm)],[t76429,t76399]) ).
cnf(t91386,plain,
qtd3(X1,qtd3(X3,qtd3(X2,qtd4))) = qtd3(qtd0(X3,X1),qtd3(X2,qtd4)),
inference(step,[status(thm)],[t91385,t76399]) ).
cnf(t81332,plain,
qtd3(qtd0(X1,X2),qtd3(X3,qtd4)) = qtd3(X2,qtd3(X1,qtd3(X3,qtd4))),
inference(orient,[status(thm)],[t91386]) ).
cnf(t81364,plain,
qtd3(X1,qtd3(X2,qtd3(qtd3(qtd3(qtd3(qtd4,qtd4),X3),qtd4),qtd4))) = qtd3(qtd0(X2,X1),qtd3(qtd3(qtd4,qtd4),X3)),
inference(cp,[status(thm)],[t81332,t7723]) ).
cnf(t91387,plain,
qtd3(X1,qtd3(X2,qtd3(qtd3(qtd4,qtd4),X3))) = qtd3(qtd0(X2,X1),qtd3(qtd3(qtd4,qtd4),X3)),
inference(step,[status(thm)],[t81364,t7723]) ).
cnf(t91388,plain,
qtd3(X1,qtd3(X2,qtd3(qtd1,X3))) = qtd3(qtd0(X2,X1),qtd3(qtd3(qtd4,qtd4),X3)),
inference(step,[status(thm)],[t91387,t746]) ).
cnf(t91389,plain,
qtd3(X1,qtd3(X2,X3)) = qtd3(qtd0(X2,X1),qtd3(qtd3(qtd4,qtd4),X3)),
inference(step,[status(thm)],[t91388,t895]) ).
cnf(t91390,plain,
qtd3(X1,qtd3(X2,X3)) = qtd3(qtd0(X2,X1),qtd3(qtd1,X3)),
inference(step,[status(thm)],[t91389,t746]) ).
cnf(t91391,plain,
qtd3(X1,qtd3(X2,X3)) = qtd3(qtd0(X2,X1),X3),
inference(step,[status(thm)],[t91390,t895]) ).
cnf(t81699,plain,
qtd3(qtd0(X1,X2),X3) = qtd3(X2,qtd3(X1,X3)),
inference(orient,[status(thm)],[t91391]) ).
cnf(t81766,plain,
qtd3(X1,qtd0(X2,X3)) = qtd3(qtd3(X3,qtd3(X2,qtd4)),qtd3(X1,qtd4)),
inference(cp,[status(thm)],[t25291,t81699]) ).
cnf(t88516,plain,
qtd3(qtd3(X1,qtd3(X2,qtd4)),qtd3(X3,qtd4)) = qtd3(X3,qtd0(X2,X1)),
inference(orient,[status(thm)],[t81766]) ).
cnf(t169,plain,
ifeq(qtd2(X1,X2),true,qtd2(qtd0(X1,X3),qtd0(X2,X3)),true) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t546,plain,
ifeq(qtd2(X1,X2),true,qtd2(qtd0(X1,X3),qtd0(X2,X3)),true) = true,
inference(orient,[status(thm)],[t169]) ).
cnf(t680,plain,
true = ifeq(qtd2(X1,qtd1),true,qtd2(qtd0(X1,X2),X2),true),
inference(cp,[status(thm)],[t546,t676]) ).
cnf(t90619,plain,
true = ifeq(true,true,qtd2(qtd0(X1,X2),X2),true),
inference(step,[status(thm)],[t680,t344]) ).
cnf(t90620,plain,
true = qtd2(qtd0(X1,X2),X2),
inference(step,[status(thm)],[t90619,t257]) ).
cnf(t796,plain,
qtd2(qtd0(X1,X2),X2) = true,
inference(orient,[status(thm)],[t90620]) ).
cnf(t797,plain,
true = qtd2(qtd0(X1,qtd0(X2,X3)),X3),
inference(cp,[status(thm)],[t796,t293]) ).
cnf(t1016,plain,
qtd2(qtd0(X1,qtd0(X2,X3)),X3) = true,
inference(orient,[status(thm)],[t797]) ).
cnf(t1018,plain,
true = qtd2(qtd0(qtd0(X1,X2),X3),X2),
inference(cp,[status(thm)],[t1016,t290]) ).
cnf(t90637,plain,
true = qtd2(qtd0(X1,qtd0(X2,X3)),X2),
inference(step,[status(thm)],[t1018,t293]) ).
cnf(t1088,plain,
qtd2(qtd0(X1,qtd0(X2,X3)),X2) = true,
inference(orient,[status(thm)],[t90637]) ).
cnf(t1093,plain,
true = ifeq(true,true,qtd2(qtd0(X1,X2),qtd3(X3,X1)),true),
inference(cp,[status(thm)],[t656,t1088]) ).
cnf(t90642,plain,
true = qtd2(qtd0(X1,X2),qtd3(X3,X1)),
inference(step,[status(thm)],[t1093,t257]) ).
cnf(t1197,plain,
qtd2(qtd0(X1,X2),qtd3(X3,X1)) = true,
inference(orient,[status(thm)],[t90642]) ).
cnf(t1202,plain,
true = ifeq(true,true,qtd2(X1,qtd3(X2,qtd3(X3,X2))),true),
inference(cp,[status(thm)],[t656,t1197]) ).
cnf(t90644,plain,
true = qtd2(X1,qtd3(X2,qtd3(X3,X2))),
inference(step,[status(thm)],[t1202,t257]) ).
cnf(t1260,plain,
qtd2(X1,qtd3(X2,qtd3(X3,X2))) = true,
inference(orient,[status(thm)],[t90644]) ).
cnf(t1262,plain,
qtd3(X1,qtd3(X2,X1)) = ifeq(true,true,qtd1,qtd3(X1,qtd3(X2,X1))),
inference(cp,[status(thm)],[t993,t1260]) ).
cnf(t90645,plain,
qtd3(X1,qtd3(X2,X1)) = qtd1,
inference(step,[status(thm)],[t1262,t257]) ).
cnf(t1271,plain,
qtd3(X1,qtd3(X2,X1)) = qtd1,
inference(orient,[status(thm)],[t90645]) ).
cnf(t1288,plain,
qtd3(qtd3(qtd3(X1,X2),X2),X2) = qtd3(qtd1,qtd3(X1,X2)),
inference(cp,[status(thm)],[t282,t1271]) ).
cnf(t90647,plain,
qtd3(qtd3(qtd3(X1,X2),X2),X2) = qtd3(X1,X2),
inference(step,[status(thm)],[t1288,t895]) ).
cnf(t1329,plain,
qtd3(qtd3(qtd3(X1,X2),X2),X2) = qtd3(X1,X2),
inference(orient,[status(thm)],[t90647]) ).
cnf(t1330,plain,
qtd3(X1,X2) = qtd3(qtd3(qtd3(X2,X1),X1),X2),
inference(cp,[status(thm)],[t1329,t282]) ).
cnf(t1361,plain,
qtd3(qtd3(qtd3(X1,X2),X2),X1) = qtd3(X2,X1),
inference(orient,[status(thm)],[t1330]) ).
cnf(t88521,plain,
qtd3(X1,qtd0(X2,qtd3(qtd3(X1,qtd4),qtd3(X2,qtd4)))) = qtd3(qtd3(X2,qtd4),qtd3(X1,qtd4)),
inference(cp,[status(thm)],[t88516,t1361]) ).
cnf(t76439,plain,
qtd0(X1,X2) = qtd3(qtd3(X2,qtd3(X1,qtd4)),qtd4),
inference(cp,[status(thm)],[t917,t76399]) ).
cnf(t76729,plain,
qtd3(qtd3(X1,qtd3(X2,qtd4)),qtd4) = qtd0(X2,X1),
inference(orient,[status(thm)],[t76439]) ).
cnf(t76764,plain,
qtd0(X1,qtd3(X2,qtd4)) = qtd3(qtd3(X1,X2),qtd4),
inference(cp,[status(thm)],[t76729,t25291]) ).
cnf(t77070,plain,
qtd0(X1,qtd3(X2,qtd4)) = qtd3(qtd3(X1,X2),qtd4),
inference(orient,[status(thm)],[t76764]) ).
cnf(t81765,plain,
qtd3(qtd3(X1,qtd0(X2,X3)),qtd4) = qtd0(X1,qtd3(X3,qtd3(X2,qtd4))),
inference(cp,[status(thm)],[t77070,t81699]) ).
cnf(t86045,plain,
qtd0(X1,qtd3(X2,qtd3(X3,qtd4))) = qtd3(qtd3(X1,qtd0(X3,X2)),qtd4),
inference(orient,[status(thm)],[t81765]) ).
cnf(t91494,plain,
qtd3(X1,qtd3(qtd3(X2,qtd0(X2,qtd3(X1,qtd4))),qtd4)) = qtd3(qtd3(X2,qtd4),qtd3(X1,qtd4)),
inference(step,[status(thm)],[t88521,t86045]) ).
cnf(t91495,plain,
qtd3(X1,qtd3(qtd3(X2,qtd3(qtd3(X2,X1),qtd4)),qtd4)) = qtd3(qtd3(X2,qtd4),qtd3(X1,qtd4)),
inference(step,[status(thm)],[t91494,t77070]) ).
cnf(t91496,plain,
qtd3(X1,qtd0(qtd3(X2,X1),X2)) = qtd3(qtd3(X2,qtd4),qtd3(X1,qtd4)),
inference(step,[status(thm)],[t91495,t76729]) ).
cnf(t91497,plain,
qtd3(X1,qtd0(X2,qtd3(X2,X1))) = qtd3(qtd3(X2,qtd4),qtd3(X1,qtd4)),
inference(step,[status(thm)],[t91496,t290]) ).
cnf(t91498,plain,
qtd3(X1,qtd0(X2,qtd3(X2,X1))) = qtd3(X1,X2),
inference(step,[status(thm)],[t91497,t25291]) ).
cnf(t88789,plain,
qtd3(X1,qtd0(X2,qtd3(X2,X1))) = qtd3(X1,X2),
inference(orient,[status(thm)],[t91498]) ).
cnf(t88938,plain,
qtd3(qtd3(qtd0(X1,qtd3(X1,X2)),X2),X2) = qtd3(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd0(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2))))),
inference(cp,[status(thm)],[t2818,t88789]) ).
cnf(t91502,plain,
qtd3(qtd1,X2) = qtd3(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd0(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2))))),
inference(step,[status(thm)],[t88938,t288]) ).
cnf(t91503,plain,
X2 = qtd3(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd0(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2))))),
inference(step,[status(thm)],[t91502,t895]) ).
cnf(t91504,plain,
X2 = qtd3(qtd1,qtd0(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2))))),
inference(step,[status(thm)],[t91503,t288]) ).
cnf(t91505,plain,
X2 = qtd0(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2)))),
inference(step,[status(thm)],[t91504,t895]) ).
cnf(t91506,plain,
X2 = qtd0(qtd1,qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2)))),
inference(step,[status(thm)],[t91505,t288]) ).
cnf(t91507,plain,
X2 = qtd3(qtd3(X2,X1),qtd0(X1,qtd3(X1,X2))),
inference(step,[status(thm)],[t91506,t676]) ).
cnf(t89562,plain,
qtd3(qtd3(X1,X2),qtd0(X2,qtd3(X2,X1))) = X1,
inference(orient,[status(thm)],[t91507]) ).
cnf(t89664,plain,
qtd0(X1,qtd3(X1,X2)) = qtd3(qtd3(qtd0(X1,qtd3(X1,X2)),X2),qtd0(X2,qtd3(X2,X1))),
inference(cp,[status(thm)],[t89562,t88789]) ).
cnf(t91512,plain,
qtd0(X1,qtd3(X1,X2)) = qtd3(qtd1,qtd0(X2,qtd3(X2,X1))),
inference(step,[status(thm)],[t89664,t288]) ).
cnf(t91513,plain,
qtd0(X1,qtd3(X1,X2)) = qtd0(X2,qtd3(X2,X1)),
inference(step,[status(thm)],[t91512,t895]) ).
cnf(t90352,plain,
qtd0(X1,qtd3(X1,X2)) = qtd0(X2,qtd3(X2,X1)),
inference(orient,[status(thm)],[t91513]) ).
fof(f13,conjecture,
! [X17,X18] : qtd0(X17,qtd3(X17,X18)) = qtd0(X18,qtd3(X18,X17)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_14) ).
fof(f13_neg,negated_conjecture,
~ ! [X17,X18] : qtd0(X17,qtd3(X17,X18)) = qtd0(X18,qtd3(X18,X17)),
inference(negated_conjecture,[status(cth)],[f13]) ).
fof(f13_nnf,plain,
? [X17,X18] : qtd0(X17,qtd3(X17,X18)) != qtd0(X18,qtd3(X18,X17)),
inference(nnf_transformation,[status(thm)],[f13_neg]) ).
fof(f13_sk,plain,
qtd0(sk0,qtd3(sk0,sk1)) != qtd0(sk1,qtd3(sk1,sk0)),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f13_nnf]) ).
cnf(c14,plain,
qtd0(sk0,qtd3(sk0,sk1)) != qtd0(sk1,qtd3(sk1,sk0)),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(goal_0,negated_conjecture,
qtd0(sk1,qtd3(sk1,sk0)) != qtd0(sk0,qtd3(sk0,sk1)),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(g0_0,plain,
qtd0(sk1,qtd3(sk1,sk0)) != qtd0(sk1,qtd3(sk1,sk0)),
inference(rw,[status(thm)],[goal_0,t90352]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL900+1 : TPTP v9.3.1. Released v5.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n005.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 : Thu Sep 24 00:39:47 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 82.84/10.98 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 82.84/10.98 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------