%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 01:37:35 PM UTC 2026
% Result : Unsatisfiable 7.25s 1.80s
% Output : Proof 7.25s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t46,axiom,
sFlat0 = input(i1,i2),
introduced(definition) ).
cnf(t319,plain,
input(i1,i2) = sFlat0,
inference(orient,[status(thm)],[t46]) ).
cnf(t47,axiom,
sFlat1 = output(i2,i1),
introduced(definition) ).
cnf(t320,plain,
output(i2,i1) = sFlat1,
inference(orient,[status(thm)],[t47]) ).
cnf(t48,axiom,
sFlat2 = circuit(input(i1,i2),output(i2,i1)),
introduced(definition) ).
cnf(t6369,plain,
sFlat2 = circuit(sFlat0,output(i2,i1)),
inference(step,[status(thm)],[t48,t319]) ).
cnf(t6370,plain,
sFlat2 = circuit(sFlat0,sFlat1),
inference(step,[status(thm)],[t6369,t320]) ).
cnf(t321,plain,
circuit(sFlat0,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t6370]) ).
cnf(f45,negated_conjecture,
circuit(input(i1,i2),output(a1,a2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',circuit_description) ).
fof(f45_nnf,plain,
circuit(input(i1,i2),output(a1,a2)),
inference(nnf_transformation,[status(thm)],[f45]) ).
cnf(c45,plain,
circuit(input(i1,i2),output(a1,a2)),
inference(cnf_transformation,[status(esa)],[f45_nnf]) ).
cnf(t34,plain,
circuit(input(i1,i2),output(a1,a2)) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
cnf(t6371,plain,
circuit(sFlat0,output(a1,a2)) = true,
inference(step,[status(thm)],[t34,t319]) ).
cnf(t322,plain,
circuit(sFlat0,output(a1,a2)) = true,
inference(orient,[status(thm)],[t6371]) ).
cnf(f27,axiom,
not(not(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_simplification) ).
fof(f27_nnf,plain,
! [X] : not(not(X)) = X,
inference(nnf_transformation,[status(thm)],[f27]) ).
fof(f27_sk,plain,
! [X] : not(not(X)) = X,
inference(skolemisation,[status(esa)],[f27_nnf]) ).
cnf(c27,plain,
not(not(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f27_sk]) ).
cnf(t15,plain,
not(not(X1)) = X1,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t61,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t15]) ).
cnf(f28,axiom,
or(and(X,Y),and(X,not(Y))) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification1) ).
fof(f28_nnf,plain,
! [X,Y] : or(and(X,Y),and(X,not(Y))) = X,
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X,Y] : or(and(X,Y),and(X,not(Y))) = X,
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
or(and(X0,X1),and(X0,not(X1))) = X0,
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t38,plain,
or(and(X1,X2),and(X1,not(X2))) = X1,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t57,plain,
or(and(X1,X2),and(X1,not(X2))) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(f16,axiom,
and(and(X,Y),Y) = and(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification2) ).
fof(f16_nnf,plain,
! [X,Y] : and(and(X,Y),Y) = and(X,Y),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X,Y] : and(and(X,Y),Y) = and(X,Y),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
and(and(X0,X1),X1) = and(X0,X1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t33,plain,
and(and(X1,X2),X2) = and(X1,X2),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(f6,axiom,
and(X,Y) = and(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutativity) ).
fof(f6_nnf,plain,
! [X,Y] : and(X,Y) = and(Y,X),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y] : and(X,Y) = and(Y,X),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
and(X0,X1) = and(X1,X0),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t26,plain,
and(X1,X2) = and(X2,X1),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t64,plain,
and(X1,X2) = and(X2,X1),
inference(orient,[status(thm)],[t26]) ).
cnf(t6353,plain,
and(X2,and(X1,X2)) = and(X1,X2),
inference(step,[status(thm)],[t33,t64]) ).
cnf(t68,plain,
and(X1,and(X2,X1)) = and(X2,X1),
inference(orient,[status(thm)],[t6353]) ).
cnf(t72,plain,
X1 = or(and(X2,X1),and(X1,not(and(X2,X1)))),
inference(cp,[status(thm)],[t57,t68]) ).
cnf(t615,plain,
or(and(X1,X2),and(X2,not(and(X1,X2)))) = X2,
inference(orient,[status(thm)],[t72]) ).
cnf(f13,axiom,
not(or(X,Y)) = and(not(X),not(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization2) ).
fof(f13_nnf,plain,
! [X,Y] : not(or(X,Y)) = and(not(X),not(Y)),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X,Y] : not(or(X,Y)) = and(not(X),not(Y)),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
not(or(X0,X1)) = and(not(X0),not(X1)),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t37,plain,
and(not(X1),not(X2)) = not(or(X1,X2)),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t127,plain,
and(not(X1),not(X2)) = not(or(X1,X2)),
inference(orient,[status(thm)],[t37]) ).
cnf(f43,negated_conjecture,
f2 = not(i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor14) ).
fof(f43_nnf,plain,
f2 = not(i2),
inference(nnf_transformation,[status(thm)],[f43]) ).
cnf(c43,plain,
f2 = not(i2),
inference(cnf_transformation,[status(esa)],[f43_nnf]) ).
cnf(t6,plain,
not(i2) = f2,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(t256,plain,
not(i2) = f2,
inference(orient,[status(thm)],[t6]) ).
cnf(t257,plain,
i2 = not(f2),
inference(cp,[status(thm)],[t61,t256]) ).
cnf(t342,plain,
not(f2) = i2,
inference(orient,[status(thm)],[t257]) ).
cnf(t347,plain,
not(or(X1,f2)) = and(not(X1),i2),
inference(cp,[status(thm)],[t127,t342]) ).
cnf(t6653,plain,
not(or(X1,f2)) = and(i2,not(X1)),
inference(step,[status(thm)],[t347,t64]) ).
cnf(t3272,plain,
not(or(X1,f2)) = and(i2,not(X1)),
inference(orient,[status(thm)],[t6653]) ).
cnf(f9,axiom,
or(X,or(Y,Z)) = or(or(X,Y),Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_associativity) ).
fof(f9_nnf,plain,
! [X,Y,Z] : or(X,or(Y,Z)) = or(or(X,Y),Z),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X,Y,Z] : or(X,or(Y,Z)) = or(or(X,Y),Z),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
or(X0,or(X1,X2)) = or(or(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t43,plain,
or(or(X1,X2),X3) = or(X1,or(X2,X3)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t178,plain,
or(or(X1,X2),X3) = or(X1,or(X2,X3)),
inference(orient,[status(thm)],[t43]) ).
cnf(f20,axiom,
or(or(X,Y),X) = or(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_simplification3) ).
fof(f20_nnf,plain,
! [X,Y] : or(or(X,Y),X) = or(X,Y),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,Y] : or(or(X,Y),X) = or(X,Y),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
or(or(X0,X1),X0) = or(X0,X1),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t35,plain,
or(or(X1,X2),X1) = or(X1,X2),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(f7,axiom,
or(X,Y) = or(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutativity) ).
fof(f7_nnf,plain,
! [X,Y] : or(X,Y) = or(Y,X),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y] : or(X,Y) = or(Y,X),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
or(X0,X1) = or(X1,X0),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t27,plain,
or(X1,X2) = or(X2,X1),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t166,plain,
or(X1,X2) = or(X2,X1),
inference(orient,[status(thm)],[t27]) ).
cnf(t6360,plain,
or(X1,or(X1,X2)) = or(X1,X2),
inference(step,[status(thm)],[t35,t166]) ).
cnf(t174,plain,
or(X1,or(X1,X2)) = or(X1,X2),
inference(orient,[status(thm)],[t6360]) ).
cnf(f29,axiom,
or(and(X,Y),and(Y,not(X))) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_not_simplification2) ).
fof(f29_nnf,plain,
! [X,Y] : or(and(X,Y),and(Y,not(X))) = Y,
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [X,Y] : or(and(X,Y),and(Y,not(X))) = Y,
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
or(and(X0,X1),and(X1,not(X0))) = X1,
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(t39,plain,
or(and(X1,X2),and(X2,not(X1))) = X2,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t53,plain,
or(and(X1,X2),and(X2,not(X1))) = X2,
inference(orient,[status(thm)],[t39]) ).
cnf(t175,plain,
or(and(X1,X2),and(X2,not(X1))) = or(and(X1,X2),X2),
inference(cp,[status(thm)],[t174,t53]) ).
cnf(t6409,plain,
X2 = or(and(X1,X2),X2),
inference(step,[status(thm)],[t175,t53]) ).
cnf(t6410,plain,
X2 = or(X2,and(X1,X2)),
inference(step,[status(thm)],[t6409,t166]) ).
cnf(t498,plain,
or(X1,and(X2,X1)) = X1,
inference(orient,[status(thm)],[t6410]) ).
cnf(f44,negated_conjecture,
f3 = and(i1,i2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor15) ).
fof(f44_nnf,plain,
f3 = and(i1,i2),
inference(nnf_transformation,[status(thm)],[f44]) ).
cnf(c44,plain,
f3 = and(i1,i2),
inference(cnf_transformation,[status(esa)],[f44_nnf]) ).
cnf(t14,plain,
and(i1,i2) = f3,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(t6356,plain,
and(i2,i1) = f3,
inference(step,[status(thm)],[t14,t64]) ).
cnf(t142,plain,
and(i2,i1) = f3,
inference(orient,[status(thm)],[t6356]) ).
cnf(t502,plain,
i1 = or(i1,f3),
inference(cp,[status(thm)],[t498,t142]) ).
cnf(t514,plain,
or(i1,f3) = i1,
inference(orient,[status(thm)],[t502]) ).
cnf(t515,plain,
or(i1,or(f3,X1)) = or(i1,X1),
inference(cp,[status(thm)],[t178,t514]) ).
cnf(t5741,plain,
or(i1,or(f3,X1)) = or(i1,X1),
inference(orient,[status(thm)],[t515]) ).
cnf(f41,negated_conjecture,
e2 = or(f2,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor12) ).
fof(f41_nnf,plain,
e2 = or(f2,f3),
inference(nnf_transformation,[status(thm)],[f41]) ).
cnf(c41,plain,
e2 = or(f2,f3),
inference(cnf_transformation,[status(esa)],[f41_nnf]) ).
cnf(t23,plain,
or(f2,f3) = e2,
inference(equality_encoding,[status(esa)],[c41]) ).
cnf(t6365,plain,
or(f3,f2) = e2,
inference(step,[status(thm)],[t23,t166]) ).
cnf(t224,plain,
or(f3,f2) = e2,
inference(orient,[status(thm)],[t6365]) ).
cnf(t5749,plain,
or(i1,f2) = or(i1,e2),
inference(cp,[status(thm)],[t5741,t224]) ).
cnf(f12,axiom,
not(and(X,Y)) = or(not(X),not(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_canonicalization1) ).
fof(f12_nnf,plain,
! [X,Y] : not(and(X,Y)) = or(not(X),not(Y)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X,Y] : not(and(X,Y)) = or(not(X),not(Y)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
not(and(X0,X1)) = or(not(X0),not(X1)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t40,plain,
or(not(X1),not(X2)) = not(and(X1,X2)),
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t205,plain,
or(not(X1),not(X2)) = not(and(X1,X2)),
inference(orient,[status(thm)],[t40]) ).
cnf(f42,negated_conjecture,
f1 = not(i1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor13) ).
fof(f42_nnf,plain,
f1 = not(i1),
inference(nnf_transformation,[status(thm)],[f42]) ).
cnf(c42,plain,
f1 = not(i1),
inference(cnf_transformation,[status(esa)],[f42_nnf]) ).
cnf(t5,plain,
not(i1) = f1,
inference(equality_encoding,[status(esa)],[c42]) ).
cnf(t244,plain,
not(i1) = f1,
inference(orient,[status(thm)],[t5]) ).
cnf(t245,plain,
i1 = not(f1),
inference(cp,[status(thm)],[t61,t244]) ).
cnf(t331,plain,
not(f1) = i1,
inference(orient,[status(thm)],[t245]) ).
cnf(t332,plain,
not(and(f1,X1)) = or(i1,not(X1)),
inference(cp,[status(thm)],[t205,t331]) ).
cnf(t3094,plain,
not(and(f1,X1)) = or(i1,not(X1)),
inference(orient,[status(thm)],[t332]) ).
cnf(t335,plain,
not(or(f1,X1)) = and(i1,not(X1)),
inference(cp,[status(thm)],[t127,t331]) ).
cnf(t3140,plain,
not(or(f1,X1)) = and(i1,not(X1)),
inference(orient,[status(thm)],[t335]) ).
cnf(t225,plain,
or(f3,or(f2,X1)) = or(e2,X1),
inference(cp,[status(thm)],[t178,t224]) ).
cnf(t3863,plain,
or(f3,or(f2,X1)) = or(e2,X1),
inference(orient,[status(thm)],[t225]) ).
cnf(t247,plain,
not(and(X1,i1)) = or(not(X1),f1),
inference(cp,[status(thm)],[t205,t244]) ).
cnf(t6461,plain,
not(and(X1,i1)) = or(f1,not(X1)),
inference(step,[status(thm)],[t247,t166]) ).
cnf(t1066,plain,
not(and(X1,i1)) = or(f1,not(X1)),
inference(orient,[status(thm)],[t6461]) ).
cnf(t1067,plain,
or(f1,not(i2)) = not(f3),
inference(cp,[status(thm)],[t1066,t142]) ).
cnf(t6462,plain,
or(f1,f2) = not(f3),
inference(step,[status(thm)],[t1067,t256]) ).
cnf(t6463,plain,
or(f2,f1) = not(f3),
inference(step,[status(thm)],[t6462,t166]) ).
cnf(t1083,plain,
or(f2,f1) = not(f3),
inference(orient,[status(thm)],[t6463]) ).
cnf(t3865,plain,
or(e2,f1) = or(f3,not(f3)),
inference(cp,[status(thm)],[t3863,t1083]) ).
cnf(t6718,plain,
or(f1,e2) = or(f3,not(f3)),
inference(step,[status(thm)],[t3865,t166]) ).
cnf(f24,axiom,
or(X,not(X)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification1) ).
fof(f24_nnf,plain,
! [X] : or(X,not(X)) = n1,
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X] : or(X,not(X)) = n1,
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
or(X0,not(X0)) = n1,
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t25,plain,
or(X1,not(X1)) = n1,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t190,plain,
or(X1,not(X1)) = n1,
inference(orient,[status(thm)],[t25]) ).
cnf(t6719,plain,
or(f1,e2) = n1,
inference(step,[status(thm)],[t6718,t190]) ).
cnf(t3875,plain,
or(f1,e2) = n1,
inference(orient,[status(thm)],[t6719]) ).
cnf(t3876,plain,
and(i1,not(e2)) = not(n1),
inference(cp,[status(thm)],[t3140,t3875]) ).
cnf(f39,negated_conjecture,
d2 = not(e2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor10) ).
fof(f39_nnf,plain,
d2 = not(e2),
inference(nnf_transformation,[status(thm)],[f39]) ).
cnf(c39,plain,
d2 = not(e2),
inference(cnf_transformation,[status(esa)],[f39_nnf]) ).
cnf(t4,plain,
not(e2) = d2,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(t304,plain,
not(e2) = d2,
inference(orient,[status(thm)],[t4]) ).
cnf(t6720,plain,
and(i1,d2) = not(n1),
inference(step,[status(thm)],[t3876,t304]) ).
cnf(f5,axiom,
not(n1) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_definition2) ).
fof(f5_nnf,plain,
not(n1) = n0,
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
not(n1) = n0,
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
cnf(t8,plain,
not(n1) = n0,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t232,plain,
not(n1) = n0,
inference(orient,[status(thm)],[t8]) ).
cnf(t6721,plain,
and(i1,d2) = n0,
inference(step,[status(thm)],[t6720,t232]) ).
cnf(t3879,plain,
and(i1,d2) = n0,
inference(orient,[status(thm)],[t6721]) ).
cnf(t3884,plain,
d2 = or(n0,and(d2,not(i1))),
inference(cp,[status(thm)],[t53,t3879]) ).
cnf(f21,axiom,
and(X,not(X)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification1) ).
fof(f21_nnf,plain,
! [X] : and(X,not(X)) = n0,
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X] : and(X,not(X)) = n0,
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
and(X0,not(X0)) = n0,
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t24,plain,
and(X1,not(X1)) = n0,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t90,plain,
and(X1,not(X1)) = n0,
inference(orient,[status(thm)],[t24]) ).
cnf(t97,plain,
X1 = or(n0,and(X1,not(not(X1)))),
inference(cp,[status(thm)],[t57,t90]) ).
cnf(t6380,plain,
X1 = or(n0,and(X1,X1)),
inference(step,[status(thm)],[t97,t61]) ).
cnf(f15,axiom,
and(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_simplification1) ).
fof(f15_nnf,plain,
! [X] : and(X,X) = X,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X] : and(X,X) = X,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
and(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t9,plain,
and(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t49,plain,
and(X1,X1) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t6381,plain,
X1 = or(n0,X1),
inference(step,[status(thm)],[t6380,t49]) ).
cnf(t356,plain,
or(n0,X1) = X1,
inference(orient,[status(thm)],[t6381]) ).
cnf(t6722,plain,
d2 = and(d2,not(i1)),
inference(step,[status(thm)],[t3884,t356]) ).
cnf(t6723,plain,
d2 = and(d2,f1),
inference(step,[status(thm)],[t6722,t244]) ).
cnf(t6724,plain,
d2 = and(f1,d2),
inference(step,[status(thm)],[t6723,t64]) ).
cnf(t3889,plain,
and(f1,d2) = d2,
inference(orient,[status(thm)],[t6724]) ).
cnf(t3890,plain,
or(i1,not(d2)) = not(d2),
inference(cp,[status(thm)],[t3094,t3889]) ).
cnf(f33,negated_conjecture,
b2 = not(d2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor4) ).
fof(f33_nnf,plain,
b2 = not(d2),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
b2 = not(d2),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(t2,plain,
not(d2) = b2,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t280,plain,
not(d2) = b2,
inference(orient,[status(thm)],[t2]) ).
cnf(t305,plain,
e2 = not(d2),
inference(cp,[status(thm)],[t61,t304]) ).
cnf(t6376,plain,
e2 = b2,
inference(step,[status(thm)],[t305,t280]) ).
cnf(t327,plain,
b2 = e2,
inference(orient,[status(thm)],[t6376]) ).
cnf(t6377,plain,
not(d2) = e2,
inference(step,[status(thm)],[t280,t327]) ).
cnf(t328,plain,
not(d2) = e2,
inference(orient,[status(thm)],[t6377]) ).
cnf(t6728,plain,
or(i1,e2) = not(d2),
inference(step,[status(thm)],[t3890,t328]) ).
cnf(t6729,plain,
or(i1,e2) = e2,
inference(step,[status(thm)],[t6728,t328]) ).
cnf(t3916,plain,
or(i1,e2) = e2,
inference(orient,[status(thm)],[t6729]) ).
cnf(t6861,plain,
or(i1,f2) = e2,
inference(step,[status(thm)],[t5749,t3916]) ).
cnf(t5755,plain,
or(i1,f2) = e2,
inference(orient,[status(thm)],[t6861]) ).
cnf(t5764,plain,
and(i2,not(i1)) = not(e2),
inference(cp,[status(thm)],[t3272,t5755]) ).
cnf(t6870,plain,
and(i2,f1) = not(e2),
inference(step,[status(thm)],[t5764,t244]) ).
cnf(t6871,plain,
and(i2,f1) = d2,
inference(step,[status(thm)],[t6870,t304]) ).
cnf(t5771,plain,
and(i2,f1) = d2,
inference(orient,[status(thm)],[t6871]) ).
cnf(t5785,plain,
f1 = or(d2,and(f1,not(and(i2,f1)))),
inference(cp,[status(thm)],[t615,t5771]) ).
cnf(t258,plain,
not(and(i2,X1)) = or(f2,not(X1)),
inference(cp,[status(thm)],[t205,t256]) ).
cnf(t1203,plain,
not(and(i2,X1)) = or(f2,not(X1)),
inference(orient,[status(thm)],[t258]) ).
cnf(t6879,plain,
f1 = or(d2,and(f1,or(f2,not(f1)))),
inference(step,[status(thm)],[t5785,t1203]) ).
cnf(t6880,plain,
f1 = or(d2,and(f1,or(f2,i1))),
inference(step,[status(thm)],[t6879,t331]) ).
cnf(f14,axiom,
and(or(X,Y),Z) = or(and(X,Z),and(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_or_canonicalization) ).
fof(f14_nnf,plain,
! [X,Y,Z] : and(or(X,Y),Z) = or(and(X,Z),and(Y,Z)),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X,Y,Z] : and(or(X,Y),Z) = or(and(X,Z),and(Y,Z)),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
and(or(X0,X1),X2) = or(and(X0,X2),and(X1,X2)),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t45,plain,
or(and(X1,X2),and(X3,X2)) = and(or(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t111,plain,
or(and(X1,X2),and(X3,X2)) = and(or(X1,X3),X2),
inference(orient,[status(thm)],[t45]) ).
cnf(t251,plain,
n0 = and(i1,f1),
inference(cp,[status(thm)],[t90,t244]) ).
cnf(t414,plain,
and(i1,f1) = n0,
inference(orient,[status(thm)],[t251]) ).
cnf(t416,plain,
and(or(X1,i1),f1) = or(and(X1,f1),n0),
inference(cp,[status(thm)],[t111,t414]) ).
cnf(t6768,plain,
and(f1,or(X1,i1)) = or(and(X1,f1),n0),
inference(step,[status(thm)],[t416,t64]) ).
cnf(f2,axiom,
or(X,n0) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_definition1) ).
fof(f2_nnf,plain,
! [X] : or(X,n0) = X,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : or(X,n0) = X,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
or(X0,n0) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t17,plain,
or(X1,n0) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t52,plain,
or(X1,n0) = X1,
inference(orient,[status(thm)],[t17]) ).
cnf(t6769,plain,
and(f1,or(X1,i1)) = and(X1,f1),
inference(step,[status(thm)],[t6768,t52]) ).
cnf(t4507,plain,
and(f1,or(X1,i1)) = and(X1,f1),
inference(orient,[status(thm)],[t6769]) ).
cnf(t6881,plain,
f1 = or(d2,and(f2,f1)),
inference(step,[status(thm)],[t6880,t4507]) ).
cnf(t249,plain,
not(or(i1,X1)) = and(f1,not(X1)),
inference(cp,[status(thm)],[t127,t244]) ).
cnf(t1085,plain,
not(or(i1,X1)) = and(f1,not(X1)),
inference(orient,[status(thm)],[t249]) ).
cnf(f34,negated_conjecture,
b3 = or(c1,c2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor5) ).
fof(f34_nnf,plain,
b3 = or(c1,c2),
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
b3 = or(c1,c2),
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(t19,plain,
or(c1,c2) = b3,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t6364,plain,
or(c2,c1) = b3,
inference(step,[status(thm)],[t19,t166]) ).
cnf(t220,plain,
or(c2,c1) = b3,
inference(orient,[status(thm)],[t6364]) ).
cnf(f32,negated_conjecture,
b1 = not(d1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor3) ).
fof(f32_nnf,plain,
b1 = not(d1),
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
b1 = not(d1),
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t1,plain,
not(d1) = b1,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t268,plain,
not(d1) = b1,
inference(orient,[status(thm)],[t1]) ).
cnf(t274,plain,
not(or(X1,d1)) = and(not(X1),b1),
inference(cp,[status(thm)],[t127,t268]) ).
cnf(t6527,plain,
not(or(X1,d1)) = and(b1,not(X1)),
inference(step,[status(thm)],[t274,t64]) ).
cnf(f38,negated_conjecture,
d1 = not(e1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor9) ).
fof(f38_nnf,plain,
d1 = not(e1),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
d1 = not(e1),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
cnf(t3,plain,
not(e1) = d1,
inference(equality_encoding,[status(esa)],[c38]) ).
cnf(t292,plain,
not(e1) = d1,
inference(orient,[status(thm)],[t3]) ).
cnf(t293,plain,
e1 = not(d1),
inference(cp,[status(thm)],[t61,t292]) ).
cnf(t6372,plain,
e1 = b1,
inference(step,[status(thm)],[t293,t268]) ).
cnf(t323,plain,
b1 = e1,
inference(orient,[status(thm)],[t6372]) ).
cnf(t6528,plain,
not(or(X1,d1)) = and(e1,not(X1)),
inference(step,[status(thm)],[t6527,t323]) ).
cnf(t1819,plain,
not(or(X1,d1)) = and(e1,not(X1)),
inference(orient,[status(thm)],[t6528]) ).
cnf(f35,negated_conjecture,
c1 = or(d1,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor6) ).
fof(f35_nnf,plain,
c1 = or(d1,d3),
inference(nnf_transformation,[status(thm)],[f35]) ).
cnf(c35,plain,
c1 = or(d1,d3),
inference(cnf_transformation,[status(esa)],[f35_nnf]) ).
cnf(t20,plain,
or(d1,d3) = c1,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t6362,plain,
or(d3,d1) = c1,
inference(step,[status(thm)],[t20,t166]) ).
cnf(t212,plain,
or(d3,d1) = c1,
inference(orient,[status(thm)],[t6362]) ).
cnf(f37,negated_conjecture,
d3 = f3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor8) ).
fof(f37_nnf,plain,
d3 = f3,
inference(nnf_transformation,[status(thm)],[f37]) ).
cnf(c37,plain,
d3 = f3,
inference(cnf_transformation,[status(esa)],[f37_nnf]) ).
cnf(t0,plain,
f3 = d3,
inference(equality_encoding,[status(esa)],[c37]) ).
cnf(t316,plain,
d3 = f3,
inference(orient,[status(thm)],[t0]) ).
cnf(t6368,plain,
or(f3,d1) = c1,
inference(step,[status(thm)],[t212,t316]) ).
cnf(t318,plain,
or(f3,d1) = c1,
inference(rw,[status(thm)],[t6368]) ).
cnf(t440,plain,
or(f3,d1) = c1,
inference(orient,[status(thm)],[t318]) ).
cnf(t1824,plain,
and(e1,not(f3)) = not(c1),
inference(cp,[status(thm)],[t1819,t440]) ).
cnf(t273,plain,
not(or(d1,X1)) = and(b1,not(X1)),
inference(cp,[status(thm)],[t127,t268]) ).
cnf(t6506,plain,
not(or(d1,X1)) = and(e1,not(X1)),
inference(step,[status(thm)],[t273,t323]) ).
cnf(t1627,plain,
not(or(d1,X1)) = and(e1,not(X1)),
inference(orient,[status(thm)],[t6506]) ).
cnf(t62,plain,
X1 = or(and(not(X2),X1),and(X1,X2)),
inference(cp,[status(thm)],[t53,t61]) ).
cnf(t6382,plain,
X1 = or(and(X1,X2),and(not(X2),X1)),
inference(step,[status(thm)],[t62,t166]) ).
cnf(t357,plain,
or(and(X1,X2),and(not(X2),X1)) = X1,
inference(orient,[status(thm)],[t6382]) ).
cnf(f26,axiom,
or(or(X,Y),not(X)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_not_simplification3) ).
fof(f26_nnf,plain,
! [X,Y] : or(or(X,Y),not(X)) = n1,
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X,Y] : or(or(X,Y),not(X)) = n1,
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
or(or(X0,X1),not(X0)) = n1,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t30,plain,
or(or(X1,X2),not(X1)) = n1,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t6361,plain,
or(X1,or(X2,not(X1))) = n1,
inference(step,[status(thm)],[t30,t178]) ).
cnf(t199,plain,
or(X1,or(X2,not(X1))) = n1,
inference(orient,[status(thm)],[t6361]) ).
cnf(t253,plain,
n1 = or(i1,or(X1,f1)),
inference(cp,[status(thm)],[t199,t244]) ).
cnf(t538,plain,
or(i1,or(X1,f1)) = n1,
inference(orient,[status(thm)],[t253]) ).
cnf(f40,negated_conjecture,
e1 = or(f1,f3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor11) ).
fof(f40_nnf,plain,
e1 = or(f1,f3),
inference(nnf_transformation,[status(thm)],[f40]) ).
cnf(c40,plain,
e1 = or(f1,f3),
inference(cnf_transformation,[status(esa)],[f40_nnf]) ).
cnf(t22,plain,
or(f1,f3) = e1,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(t6366,plain,
or(f3,f1) = e1,
inference(step,[status(thm)],[t22,t166]) ).
cnf(t228,plain,
or(f3,f1) = e1,
inference(orient,[status(thm)],[t6366]) ).
cnf(t539,plain,
n1 = or(i1,e1),
inference(cp,[status(thm)],[t538,t228]) ).
cnf(t543,plain,
or(i1,e1) = n1,
inference(orient,[status(thm)],[t539]) ).
cnf(t1088,plain,
and(f1,not(e1)) = not(n1),
inference(cp,[status(thm)],[t1085,t543]) ).
cnf(t6464,plain,
and(f1,d1) = not(n1),
inference(step,[status(thm)],[t1088,t292]) ).
cnf(t6465,plain,
and(f1,d1) = n0,
inference(step,[status(thm)],[t6464,t232]) ).
cnf(t1109,plain,
and(f1,d1) = n0,
inference(orient,[status(thm)],[t6465]) ).
cnf(t1113,plain,
d1 = or(n0,and(d1,not(f1))),
inference(cp,[status(thm)],[t53,t1109]) ).
cnf(t6466,plain,
d1 = and(d1,not(f1)),
inference(step,[status(thm)],[t1113,t356]) ).
cnf(t6467,plain,
d1 = and(d1,i1),
inference(step,[status(thm)],[t6466,t331]) ).
cnf(t6468,plain,
d1 = and(i1,d1),
inference(step,[status(thm)],[t6467,t64]) ).
cnf(t1116,plain,
and(i1,d1) = d1,
inference(orient,[status(thm)],[t6468]) ).
cnf(t1121,plain,
i1 = or(d1,and(not(d1),i1)),
inference(cp,[status(thm)],[t357,t1116]) ).
cnf(t6475,plain,
i1 = or(d1,and(i1,not(d1))),
inference(step,[status(thm)],[t1121,t64]) ).
cnf(t6373,plain,
not(d1) = e1,
inference(step,[status(thm)],[t268,t323]) ).
cnf(t324,plain,
not(d1) = e1,
inference(orient,[status(thm)],[t6373]) ).
cnf(t6476,plain,
i1 = or(d1,and(i1,e1)),
inference(step,[status(thm)],[t6475,t324]) ).
cnf(t1163,plain,
or(d1,and(i1,e1)) = i1,
inference(orient,[status(thm)],[t6476]) ).
cnf(t1630,plain,
and(e1,not(and(i1,e1))) = not(i1),
inference(cp,[status(thm)],[t1627,t1163]) ).
cnf(t246,plain,
not(and(i1,X1)) = or(f1,not(X1)),
inference(cp,[status(thm)],[t205,t244]) ).
cnf(t1046,plain,
not(and(i1,X1)) = or(f1,not(X1)),
inference(orient,[status(thm)],[t246]) ).
cnf(t6511,plain,
and(e1,or(f1,not(e1))) = not(i1),
inference(step,[status(thm)],[t1630,t1046]) ).
cnf(t6512,plain,
and(e1,or(f1,d1)) = not(i1),
inference(step,[status(thm)],[t6511,t292]) ).
cnf(f23,axiom,
and(and(X,Y),not(X)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_not_simplification3) ).
fof(f23_nnf,plain,
! [X,Y] : and(and(X,Y),not(X)) = n0,
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X,Y] : and(and(X,Y),not(X)) = n0,
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
and(and(X0,X1),not(X0)) = n0,
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t28,plain,
and(and(X1,X2),not(X1)) = n0,
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(f8,axiom,
and(X,and(Y,Z)) = and(and(X,Y),Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_associativity) ).
fof(f8_nnf,plain,
! [X,Y,Z] : and(X,and(Y,Z)) = and(and(X,Y),Z),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X,Y,Z] : and(X,and(Y,Z)) = and(and(X,Y),Z),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
and(X0,and(X1,X2)) = and(and(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t41,plain,
and(and(X1,X2),X3) = and(X1,and(X2,X3)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t77,plain,
and(and(X1,X2),X3) = and(X1,and(X2,X3)),
inference(orient,[status(thm)],[t41]) ).
cnf(t6355,plain,
and(X1,and(X2,not(X1))) = n0,
inference(step,[status(thm)],[t28,t77]) ).
cnf(t103,plain,
and(X1,and(X2,not(X1))) = n0,
inference(orient,[status(thm)],[t6355]) ).
cnf(t340,plain,
n0 = and(f1,and(X1,i1)),
inference(cp,[status(thm)],[t103,t331]) ).
cnf(t663,plain,
and(f1,and(X1,i1)) = n0,
inference(orient,[status(thm)],[t340]) ).
cnf(t667,plain,
n0 = and(f1,f3),
inference(cp,[status(thm)],[t663,t142]) ).
cnf(t6417,plain,
n0 = and(f3,f1),
inference(step,[status(thm)],[t667,t64]) ).
cnf(t675,plain,
and(f3,f1) = n0,
inference(orient,[status(thm)],[t6417]) ).
cnf(t679,plain,
f1 = or(n0,and(f1,not(f3))),
inference(cp,[status(thm)],[t53,t675]) ).
cnf(t6418,plain,
f1 = and(f1,not(f3)),
inference(step,[status(thm)],[t679,t356]) ).
cnf(t681,plain,
and(f1,not(f3)) = f1,
inference(orient,[status(thm)],[t6418]) ).
cnf(t687,plain,
not(f3) = or(f1,and(not(f3),not(f1))),
inference(cp,[status(thm)],[t53,t681]) ).
cnf(t6419,plain,
not(f3) = or(f1,not(or(f3,f1))),
inference(step,[status(thm)],[t687,t127]) ).
cnf(t6420,plain,
not(f3) = or(f1,not(e1)),
inference(step,[status(thm)],[t6419,t228]) ).
cnf(t6421,plain,
not(f3) = or(f1,d1),
inference(step,[status(thm)],[t6420,t292]) ).
cnf(t690,plain,
or(f1,d1) = not(f3),
inference(orient,[status(thm)],[t6421]) ).
cnf(t6513,plain,
and(e1,not(f3)) = not(i1),
inference(step,[status(thm)],[t6512,t690]) ).
cnf(t6514,plain,
and(e1,not(f3)) = f1,
inference(step,[status(thm)],[t6513,t244]) ).
cnf(t1669,plain,
and(e1,not(f3)) = f1,
inference(orient,[status(thm)],[t6514]) ).
cnf(t6529,plain,
f1 = not(c1),
inference(step,[status(thm)],[t1824,t1669]) ).
cnf(t1838,plain,
not(c1) = f1,
inference(orient,[status(thm)],[t6529]) ).
cnf(t1839,plain,
c1 = not(f1),
inference(cp,[status(thm)],[t61,t1838]) ).
cnf(t6535,plain,
c1 = i1,
inference(step,[status(thm)],[t1839,t331]) ).
cnf(t1855,plain,
c1 = i1,
inference(orient,[status(thm)],[t6535]) ).
cnf(t6547,plain,
or(c2,i1) = b3,
inference(step,[status(thm)],[t220,t1855]) ).
cnf(t1865,plain,
or(c2,i1) = b3,
inference(rw,[status(thm)],[t6547]) ).
cnf(t6555,plain,
or(i1,c2) = b3,
inference(step,[status(thm)],[t1865,t166]) ).
cnf(t1888,plain,
or(i1,c2) = b3,
inference(orient,[status(thm)],[t6555]) ).
cnf(t1890,plain,
and(f1,not(c2)) = not(b3),
inference(cp,[status(thm)],[t1085,t1888]) ).
cnf(t2025,plain,
and(f1,not(c2)) = not(b3),
inference(orient,[status(thm)],[t1890]) ).
cnf(t286,plain,
not(or(X1,d2)) = and(not(X1),b2),
inference(cp,[status(thm)],[t127,t280]) ).
cnf(t6600,plain,
not(or(X1,d2)) = and(b2,not(X1)),
inference(step,[status(thm)],[t286,t64]) ).
cnf(t6601,plain,
not(or(X1,d2)) = and(e2,not(X1)),
inference(step,[status(thm)],[t6600,t327]) ).
cnf(t2377,plain,
not(or(X1,d2)) = and(e2,not(X1)),
inference(orient,[status(thm)],[t6601]) ).
cnf(f36,negated_conjecture,
c2 = or(d2,d3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor7) ).
fof(f36_nnf,plain,
c2 = or(d2,d3),
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c36,plain,
c2 = or(d2,d3),
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(t21,plain,
or(d2,d3) = c2,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(t6363,plain,
or(d3,d2) = c2,
inference(step,[status(thm)],[t21,t166]) ).
cnf(t216,plain,
or(d3,d2) = c2,
inference(orient,[status(thm)],[t6363]) ).
cnf(t6367,plain,
or(f3,d2) = c2,
inference(step,[status(thm)],[t216,t316]) ).
cnf(t317,plain,
or(f3,d2) = c2,
inference(rw,[status(thm)],[t6367]) ).
cnf(t436,plain,
or(f3,d2) = c2,
inference(orient,[status(thm)],[t317]) ).
cnf(t2383,plain,
and(e2,not(f3)) = not(c2),
inference(cp,[status(thm)],[t2377,t436]) ).
cnf(t285,plain,
not(or(d2,X1)) = and(b2,not(X1)),
inference(cp,[status(thm)],[t127,t280]) ).
cnf(t6578,plain,
not(or(d2,X1)) = and(e2,not(X1)),
inference(step,[status(thm)],[t285,t327]) ).
cnf(t2175,plain,
not(or(d2,X1)) = and(e2,not(X1)),
inference(orient,[status(thm)],[t6578]) ).
cnf(t261,plain,
not(or(i2,X1)) = and(f2,not(X1)),
inference(cp,[status(thm)],[t127,t256]) ).
cnf(t1241,plain,
not(or(i2,X1)) = and(f2,not(X1)),
inference(orient,[status(thm)],[t261]) ).
cnf(t265,plain,
n1 = or(i2,or(X1,f2)),
inference(cp,[status(thm)],[t199,t256]) ).
cnf(t553,plain,
or(i2,or(X1,f2)) = n1,
inference(orient,[status(thm)],[t265]) ).
cnf(t554,plain,
n1 = or(i2,e2),
inference(cp,[status(thm)],[t553,t224]) ).
cnf(t558,plain,
or(i2,e2) = n1,
inference(orient,[status(thm)],[t554]) ).
cnf(t1245,plain,
and(f2,not(e2)) = not(n1),
inference(cp,[status(thm)],[t1241,t558]) ).
cnf(t6481,plain,
and(f2,d2) = not(n1),
inference(step,[status(thm)],[t1245,t304]) ).
cnf(t6482,plain,
and(f2,d2) = n0,
inference(step,[status(thm)],[t6481,t232]) ).
cnf(t1266,plain,
and(f2,d2) = n0,
inference(orient,[status(thm)],[t6482]) ).
cnf(t1270,plain,
d2 = or(n0,and(d2,not(f2))),
inference(cp,[status(thm)],[t53,t1266]) ).
cnf(t6483,plain,
d2 = and(d2,not(f2)),
inference(step,[status(thm)],[t1270,t356]) ).
cnf(t6484,plain,
d2 = and(d2,i2),
inference(step,[status(thm)],[t6483,t342]) ).
cnf(t6485,plain,
d2 = and(i2,d2),
inference(step,[status(thm)],[t6484,t64]) ).
cnf(t1273,plain,
and(i2,d2) = d2,
inference(orient,[status(thm)],[t6485]) ).
cnf(t1278,plain,
i2 = or(d2,and(not(d2),i2)),
inference(cp,[status(thm)],[t357,t1273]) ).
cnf(t6492,plain,
i2 = or(d2,and(i2,not(d2))),
inference(step,[status(thm)],[t1278,t64]) ).
cnf(t6493,plain,
i2 = or(d2,and(i2,e2)),
inference(step,[status(thm)],[t6492,t328]) ).
cnf(t1320,plain,
or(d2,and(i2,e2)) = i2,
inference(orient,[status(thm)],[t6493]) ).
cnf(t2179,plain,
and(e2,not(and(i2,e2))) = not(i2),
inference(cp,[status(thm)],[t2175,t1320]) ).
cnf(t6583,plain,
and(e2,or(f2,not(e2))) = not(i2),
inference(step,[status(thm)],[t2179,t1203]) ).
cnf(t6584,plain,
and(e2,or(f2,d2)) = not(i2),
inference(step,[status(thm)],[t6583,t304]) ).
cnf(t351,plain,
n0 = and(f2,and(X1,i2)),
inference(cp,[status(thm)],[t103,t342]) ).
cnf(t708,plain,
and(f2,and(X1,i2)) = n0,
inference(orient,[status(thm)],[t351]) ).
cnf(t713,plain,
n0 = and(f2,and(i2,X1)),
inference(cp,[status(thm)],[t708,t64]) ).
cnf(t900,plain,
and(f2,and(i2,X1)) = n0,
inference(orient,[status(thm)],[t713]) ).
cnf(t901,plain,
n0 = and(f2,f3),
inference(cp,[status(thm)],[t900,t142]) ).
cnf(t6449,plain,
n0 = and(f3,f2),
inference(step,[status(thm)],[t901,t64]) ).
cnf(t910,plain,
and(f3,f2) = n0,
inference(orient,[status(thm)],[t6449]) ).
cnf(t914,plain,
f2 = or(n0,and(f2,not(f3))),
inference(cp,[status(thm)],[t53,t910]) ).
cnf(t6450,plain,
f2 = and(f2,not(f3)),
inference(step,[status(thm)],[t914,t356]) ).
cnf(t940,plain,
and(f2,not(f3)) = f2,
inference(orient,[status(thm)],[t6450]) ).
cnf(t946,plain,
not(f3) = or(f2,and(not(f3),not(f2))),
inference(cp,[status(thm)],[t53,t940]) ).
cnf(t6451,plain,
not(f3) = or(f2,not(or(f3,f2))),
inference(step,[status(thm)],[t946,t127]) ).
cnf(t6452,plain,
not(f3) = or(f2,not(e2)),
inference(step,[status(thm)],[t6451,t224]) ).
cnf(t6453,plain,
not(f3) = or(f2,d2),
inference(step,[status(thm)],[t6452,t304]) ).
cnf(t949,plain,
or(f2,d2) = not(f3),
inference(orient,[status(thm)],[t6453]) ).
cnf(t6585,plain,
and(e2,not(f3)) = not(i2),
inference(step,[status(thm)],[t6584,t949]) ).
cnf(t6586,plain,
and(e2,not(f3)) = f2,
inference(step,[status(thm)],[t6585,t256]) ).
cnf(t2219,plain,
and(e2,not(f3)) = f2,
inference(orient,[status(thm)],[t6586]) ).
cnf(t6602,plain,
f2 = not(c2),
inference(step,[status(thm)],[t2383,t2219]) ).
cnf(t2397,plain,
not(c2) = f2,
inference(orient,[status(thm)],[t6602]) ).
cnf(t6608,plain,
and(f1,f2) = not(b3),
inference(step,[status(thm)],[t2025,t2397]) ).
cnf(t2414,plain,
and(f1,f2) = not(b3),
inference(rw,[status(thm)],[t6608]) ).
cnf(t6636,plain,
and(f2,f1) = not(b3),
inference(step,[status(thm)],[t2414,t64]) ).
cnf(t2490,plain,
and(f2,f1) = not(b3),
inference(orient,[status(thm)],[t6636]) ).
cnf(t6882,plain,
f1 = or(d2,not(b3)),
inference(step,[status(thm)],[t6881,t2490]) ).
cnf(t306,plain,
not(and(e2,X1)) = or(d2,not(X1)),
inference(cp,[status(thm)],[t205,t304]) ).
cnf(t2993,plain,
not(and(e2,X1)) = or(d2,not(X1)),
inference(orient,[status(thm)],[t306]) ).
cnf(f31,negated_conjecture,
a2 = and(b2,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor2) ).
fof(f31_nnf,plain,
a2 = and(b2,b3),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
a2 = and(b2,b3),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t13,plain,
and(b2,b3) = a2,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t6358,plain,
and(b3,b2) = a2,
inference(step,[status(thm)],[t13,t64]) ).
cnf(t158,plain,
and(b3,b2) = a2,
inference(orient,[status(thm)],[t6358]) ).
cnf(t6379,plain,
and(b3,e2) = a2,
inference(step,[status(thm)],[t158,t327]) ).
cnf(t330,plain,
and(b3,e2) = a2,
inference(rw,[status(thm)],[t6379]) ).
cnf(t6400,plain,
and(e2,b3) = a2,
inference(step,[status(thm)],[t330,t64]) ).
cnf(t453,plain,
and(e2,b3) = a2,
inference(orient,[status(thm)],[t6400]) ).
cnf(t2999,plain,
or(d2,not(b3)) = not(a2),
inference(cp,[status(thm)],[t2993,t453]) ).
cnf(t3019,plain,
or(d2,not(b3)) = not(a2),
inference(orient,[status(thm)],[t2999]) ).
cnf(t6883,plain,
f1 = not(a2),
inference(step,[status(thm)],[t6882,t3019]) ).
cnf(t5794,plain,
not(a2) = f1,
inference(orient,[status(thm)],[t6883]) ).
cnf(t5797,plain,
a2 = not(f1),
inference(cp,[status(thm)],[t61,t5794]) ).
cnf(t6897,plain,
a2 = i1,
inference(step,[status(thm)],[t5797,t331]) ).
cnf(t5817,plain,
a2 = i1,
inference(orient,[status(thm)],[t6897]) ).
cnf(t6929,plain,
circuit(sFlat0,output(a1,i1)) = true,
inference(step,[status(thm)],[t322,t5817]) ).
cnf(t5843,plain,
circuit(sFlat0,output(a1,i1)) = true,
inference(rw,[status(thm)],[t6929]) ).
cnf(t437,plain,
or(f3,or(d2,X1)) = or(c2,X1),
inference(cp,[status(thm)],[t178,t436]) ).
cnf(t2398,plain,
c2 = not(f2),
inference(cp,[status(thm)],[t61,t2397]) ).
cnf(t6609,plain,
c2 = i2,
inference(step,[status(thm)],[t2398,t342]) ).
cnf(t2415,plain,
c2 = i2,
inference(orient,[status(thm)],[t6609]) ).
cnf(t6815,plain,
or(f3,or(d2,X1)) = or(i2,X1),
inference(step,[status(thm)],[t437,t2415]) ).
cnf(t4964,plain,
or(f3,or(d2,X1)) = or(i2,X1),
inference(orient,[status(thm)],[t6815]) ).
cnf(t3897,plain,
f1 = or(d2,and(not(d2),f1)),
inference(cp,[status(thm)],[t357,t3889]) ).
cnf(t6736,plain,
f1 = or(d2,and(f1,not(d2))),
inference(step,[status(thm)],[t3897,t64]) ).
cnf(t6737,plain,
f1 = or(d2,and(f1,e2)),
inference(step,[status(thm)],[t6736,t328]) ).
cnf(t3992,plain,
or(d2,and(f1,e2)) = f1,
inference(orient,[status(thm)],[t6737]) ).
cnf(t4967,plain,
or(i2,and(f1,e2)) = or(f3,f1),
inference(cp,[status(thm)],[t4964,t3992]) ).
cnf(t6824,plain,
or(i2,and(f1,e2)) = e1,
inference(step,[status(thm)],[t4967,t228]) ).
cnf(t5037,plain,
or(i2,and(f1,e2)) = e1,
inference(orient,[status(thm)],[t6824]) ).
cnf(t5040,plain,
and(f2,not(and(f1,e2))) = not(e1),
inference(cp,[status(thm)],[t1241,t5037]) ).
cnf(t6831,plain,
and(f2,or(i1,not(e2))) = not(e1),
inference(step,[status(thm)],[t5040,t3094]) ).
cnf(t6832,plain,
and(f2,or(i1,d2)) = not(e1),
inference(step,[status(thm)],[t6831,t304]) ).
cnf(t6833,plain,
and(f2,or(i1,d2)) = d1,
inference(step,[status(thm)],[t6832,t292]) ).
cnf(t5235,plain,
and(f2,or(i1,d2)) = d1,
inference(orient,[status(thm)],[t6833]) ).
cnf(t417,plain,
and(i1,and(f1,X1)) = and(n0,X1),
inference(cp,[status(thm)],[t77,t414]) ).
cnf(f0,axiom,
and(X,n0) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_definition1) ).
fof(f0_nnf,plain,
! [X] : and(X,n0) = n0,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : and(X,n0) = n0,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
and(X0,n0) = n0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t10,plain,
and(X1,n0) = n0,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t98,plain,
and(X1,n0) = n0,
inference(orient,[status(thm)],[t10]) ).
cnf(t99,plain,
n0 = and(n0,X1),
inference(cp,[status(thm)],[t98,t64]) ).
cnf(t384,plain,
and(n0,X1) = n0,
inference(orient,[status(thm)],[t99]) ).
cnf(t6427,plain,
and(i1,and(f1,X1)) = n0,
inference(step,[status(thm)],[t417,t384]) ).
cnf(t729,plain,
and(i1,and(f1,X1)) = n0,
inference(orient,[status(thm)],[t6427]) ).
cnf(f19,axiom,
or(or(X,Y),Y) = or(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_simplification2) ).
fof(f19_nnf,plain,
! [X,Y] : or(or(X,Y),Y) = or(X,Y),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X,Y] : or(or(X,Y),Y) = or(X,Y),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
or(or(X0,X1),X1) = or(X0,X1),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t36,plain,
or(or(X1,X2),X2) = or(X1,X2),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t6359,plain,
or(X2,or(X1,X2)) = or(X1,X2),
inference(step,[status(thm)],[t36,t166]) ).
cnf(t169,plain,
or(X1,or(X2,X1)) = or(X2,X1),
inference(orient,[status(thm)],[t6359]) ).
cnf(t223,plain,
or(c2,c1) = or(c1,b3),
inference(cp,[status(thm)],[t169,t220]) ).
cnf(t6386,plain,
b3 = or(c1,b3),
inference(step,[status(thm)],[t223,t220]) ).
cnf(t402,plain,
or(c1,b3) = b3,
inference(orient,[status(thm)],[t6386]) ).
cnf(t6546,plain,
or(i1,b3) = b3,
inference(step,[status(thm)],[t402,t1855]) ).
cnf(t1864,plain,
or(i1,b3) = b3,
inference(rw,[status(thm)],[t6546]) ).
cnf(t1883,plain,
or(i1,b3) = b3,
inference(orient,[status(thm)],[t1864]) ).
cnf(t1885,plain,
and(f1,not(b3)) = not(b3),
inference(cp,[status(thm)],[t1085,t1883]) ).
cnf(t1919,plain,
and(f1,not(b3)) = not(b3),
inference(orient,[status(thm)],[t1885]) ).
cnf(t1922,plain,
n0 = and(i1,not(b3)),
inference(cp,[status(thm)],[t729,t1919]) ).
cnf(t1963,plain,
and(i1,not(b3)) = n0,
inference(orient,[status(thm)],[t1922]) ).
cnf(t1967,plain,
i1 = or(and(b3,i1),n0),
inference(cp,[status(thm)],[t53,t1963]) ).
cnf(t6563,plain,
i1 = and(b3,i1),
inference(step,[status(thm)],[t1967,t52]) ).
cnf(t6564,plain,
i1 = and(i1,b3),
inference(step,[status(thm)],[t6563,t64]) ).
cnf(t1971,plain,
and(i1,b3) = i1,
inference(orient,[status(thm)],[t6564]) ).
cnf(t1979,plain,
b3 = or(i1,and(b3,not(i1))),
inference(cp,[status(thm)],[t53,t1971]) ).
cnf(t6573,plain,
b3 = or(i1,and(b3,f1)),
inference(step,[status(thm)],[t1979,t244]) ).
cnf(t6574,plain,
b3 = or(i1,and(f1,b3)),
inference(step,[status(thm)],[t6573,t64]) ).
cnf(t2117,plain,
or(i1,and(f1,b3)) = b3,
inference(orient,[status(thm)],[t6574]) ).
cnf(t6617,plain,
or(i1,i2) = b3,
inference(step,[status(thm)],[t1888,t2415]) ).
cnf(t2422,plain,
or(i1,i2) = b3,
inference(rw,[status(thm)],[t6617]) ).
cnf(t6632,plain,
or(i2,i1) = b3,
inference(step,[status(thm)],[t2422,t166]) ).
cnf(t2457,plain,
or(i2,i1) = b3,
inference(orient,[status(thm)],[t6632]) ).
cnf(t4510,plain,
and(i2,f1) = and(f1,b3),
inference(cp,[status(thm)],[t4507,t2457]) ).
cnf(t4529,plain,
and(f1,b3) = and(i2,f1),
inference(orient,[status(thm)],[t4510]) ).
cnf(t6770,plain,
or(i1,and(i2,f1)) = b3,
inference(step,[status(thm)],[t2117,t4529]) ).
cnf(t4547,plain,
or(i1,and(i2,f1)) = b3,
inference(rw,[status(thm)],[t6770]) ).
cnf(t4557,plain,
or(i1,and(i2,f1)) = b3,
inference(orient,[status(thm)],[t4547]) ).
cnf(t6877,plain,
or(i1,d2) = b3,
inference(step,[status(thm)],[t4557,t5771]) ).
cnf(t5792,plain,
or(i1,d2) = b3,
inference(rw,[status(thm)],[t6877]) ).
cnf(t6149,plain,
or(i1,d2) = b3,
inference(orient,[status(thm)],[t5792]) ).
cnf(t6932,plain,
and(f2,b3) = d1,
inference(step,[status(thm)],[t5235,t6149]) ).
cnf(t263,plain,
n0 = and(i2,f2),
inference(cp,[status(thm)],[t90,t256]) ).
cnf(t420,plain,
and(i2,f2) = n0,
inference(orient,[status(thm)],[t263]) ).
cnf(t421,plain,
and(or(i2,X1),f2) = or(n0,and(X1,f2)),
inference(cp,[status(thm)],[t111,t420]) ).
cnf(t6774,plain,
and(f2,or(i2,X1)) = or(n0,and(X1,f2)),
inference(step,[status(thm)],[t421,t64]) ).
cnf(t6775,plain,
and(f2,or(i2,X1)) = and(X1,f2),
inference(step,[status(thm)],[t6774,t356]) ).
cnf(t4562,plain,
and(f2,or(i2,X1)) = and(X1,f2),
inference(orient,[status(thm)],[t6775]) ).
cnf(t4569,plain,
and(i1,f2) = and(f2,b3),
inference(cp,[status(thm)],[t4562,t2457]) ).
cnf(t4602,plain,
and(f2,b3) = and(i1,f2),
inference(orient,[status(thm)],[t4569]) ).
cnf(t6933,plain,
and(i1,f2) = d1,
inference(step,[status(thm)],[t6932,t4602]) ).
cnf(t6154,plain,
and(i1,f2) = d1,
inference(rw,[status(thm)],[t6933]) ).
cnf(t6182,plain,
and(i1,f2) = d1,
inference(orient,[status(thm)],[t6154]) ).
cnf(t6189,plain,
f2 = or(d1,and(f2,not(i1))),
inference(cp,[status(thm)],[t53,t6182]) ).
cnf(t6943,plain,
f2 = or(d1,and(f2,f1)),
inference(step,[status(thm)],[t6189,t244]) ).
cnf(t6944,plain,
f2 = or(d1,not(b3)),
inference(step,[status(thm)],[t6943,t2490]) ).
cnf(t294,plain,
not(and(e1,X1)) = or(d1,not(X1)),
inference(cp,[status(thm)],[t205,t292]) ).
cnf(t2896,plain,
not(and(e1,X1)) = or(d1,not(X1)),
inference(orient,[status(thm)],[t294]) ).
cnf(f30,negated_conjecture,
a1 = and(b1,b3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',constructor1) ).
fof(f30_nnf,plain,
a1 = and(b1,b3),
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
a1 = and(b1,b3),
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(t12,plain,
and(b1,b3) = a1,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t6357,plain,
and(b3,b1) = a1,
inference(step,[status(thm)],[t12,t64]) ).
cnf(t150,plain,
and(b3,b1) = a1,
inference(orient,[status(thm)],[t6357]) ).
cnf(t6375,plain,
and(b3,e1) = a1,
inference(step,[status(thm)],[t150,t323]) ).
cnf(t326,plain,
and(b3,e1) = a1,
inference(rw,[status(thm)],[t6375]) ).
cnf(t6399,plain,
and(e1,b3) = a1,
inference(step,[status(thm)],[t326,t64]) ).
cnf(t444,plain,
and(e1,b3) = a1,
inference(orient,[status(thm)],[t6399]) ).
cnf(t2901,plain,
or(d1,not(b3)) = not(a1),
inference(cp,[status(thm)],[t2896,t444]) ).
cnf(t2921,plain,
or(d1,not(b3)) = not(a1),
inference(orient,[status(thm)],[t2901]) ).
cnf(t6945,plain,
f2 = not(a1),
inference(step,[status(thm)],[t6944,t2921]) ).
cnf(t6204,plain,
not(a1) = f2,
inference(orient,[status(thm)],[t6945]) ).
cnf(t6207,plain,
a1 = not(f2),
inference(cp,[status(thm)],[t61,t6204]) ).
cnf(t6955,plain,
a1 = i2,
inference(step,[status(thm)],[t6207,t342]) ).
cnf(t6225,plain,
a1 = i2,
inference(orient,[status(thm)],[t6955]) ).
cnf(t6989,plain,
circuit(sFlat0,output(i2,i1)) = true,
inference(step,[status(thm)],[t5843,t6225]) ).
cnf(t6990,plain,
circuit(sFlat0,sFlat1) = true,
inference(step,[status(thm)],[t6989,t320]) ).
cnf(t6991,plain,
sFlat2 = true,
inference(step,[status(thm)],[t6990,t321]) ).
cnf(t6352,plain,
true = sFlat2,
inference(orient,[status(thm)],[t6991]) ).
cnf(f46,negated_conjecture,
~ circuit(input(i1,i2),output(i2,i1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_interchange) ).
fof(f46_nnf,plain,
~ circuit(input(i1,i2),output(i2,i1)),
inference(nnf_transformation,[status(thm)],[f46]) ).
fof(f46_sk,plain,
~ circuit(input(i1,i2),output(i2,i1)),
inference(skolemisation,[status(esa)],[f46_nnf]) ).
cnf(c46,plain,
~ circuit(input(i1,i2),output(i2,i1)),
inference(cnf_transformation,[status(esa)],[f46_sk]) ).
cnf(goal_0,negated_conjecture,
circuit(input(i1,i2),output(i2,i1)) != true,
inference(equality_encoding,[status(esa)],[c46]) ).
cnf(g0_0,plain,
circuit(sFlat0,output(i2,i1)) != true,
inference(rw,[status(thm)],[goal_0,t319]) ).
cnf(g0_1,plain,
circuit(sFlat0,sFlat1) != true,
inference(rw,[status(thm)],[g0_0,t320]) ).
cnf(g0_2,plain,
sFlat2 != true,
inference(rw,[status(thm)],[g0_1,t321]) ).
cnf(g0_3,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_2,t6352]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : HWV001-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n017.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Wed Sep 23 16:15:15 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 7.25/1.80 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.25/1.80 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------