%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN156-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 : 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 03:33:57 PM UTC 2026
% Result : Unsatisfiable 8.73s 1.73s
% Output : Proof 8.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 28
% Syntax : Number of formulae : 154 ( 82 unt; 0 def)
% Number of atoms : 282 ( 48 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 262 ( 134 ~; 128 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 6 con; 0-4 aty)
% Number of variables : 260 ( 52 sgn 100 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f122,axiom,
( ~ p0(C,B)
| p1(B,B,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_085) ).
fof(f122_nnf,plain,
! [B,C] :
( ~ p0(C,B)
| p1(B,B,B) ),
inference(nnf_transformation,[status(thm)],[f122]) ).
fof(f122_sk,plain,
! [B,C] :
( ~ p0(C,B)
| p1(B,B,B) ),
inference(skolemisation,[status(esa)],[f122_nnf]) ).
cnf(c122,plain,
( ~ p0(X1,X0)
| p1(X0,X0,X0) ),
inference(cnf_transformation,[status(esa)],[f122_sk]) ).
cnf(hi120,axiom,
ifeq(p0(X0,X1),true,p1(X1,X1,X1),true) = true,
inference(equality_encoding,[status(esa)],[c122]) ).
cnf(f13,axiom,
p0(b,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_14) ).
fof(f13_nnf,plain,
! [X] : p0(b,X),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X] : p0(b,X),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
p0(b,X0),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
p0(b,X0) = true,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(h30,plain,
p1(V0,V0,V0) = true,
inference(hyper_resolution,[status(thm)],[hi120,hi13]) ).
cnf(f174,axiom,
( ~ p1(B,C,A)
| n2(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_137) ).
fof(f174_nnf,plain,
! [A,B,C] :
( ~ p1(B,C,A)
| n2(A) ),
inference(nnf_transformation,[status(thm)],[f174]) ).
fof(f174_sk,plain,
! [A,B,C] :
( ~ p1(B,C,A)
| n2(A) ),
inference(skolemisation,[status(esa)],[f174_nnf]) ).
cnf(c174,plain,
( ~ p1(X1,X2,X0)
| n2(X0) ),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
cnf(hi171,axiom,
ifeq(p1(X0,X1,X2),true,n2(X2),true) = true,
inference(equality_encoding,[status(esa)],[c174]) ).
cnf(h174,plain,
n2(V0) = true,
inference(hyper_resolution,[status(thm)],[hi171,h30]) ).
cnf(f273,axiom,
( ~ n2(A)
| m3(A,A,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_236) ).
fof(f273_nnf,plain,
! [A] :
( ~ n2(A)
| m3(A,A,A) ),
inference(nnf_transformation,[status(thm)],[f273]) ).
fof(f273_sk,plain,
! [A] :
( ~ n2(A)
| m3(A,A,A) ),
inference(skolemisation,[status(esa)],[f273_nnf]) ).
cnf(c273,plain,
( ~ n2(X0)
| m3(X0,X0,X0) ),
inference(cnf_transformation,[status(esa)],[f273_sk]) ).
cnf(hi268,axiom,
ifeq(n2(X0),true,m3(X0,X0,X0),true) = true,
inference(equality_encoding,[status(esa)],[c273]) ).
cnf(h219,plain,
m3(V0,V0,V0) = true,
inference(hyper_resolution,[status(thm)],[hi268,h174]) ).
cnf(f129,axiom,
( ~ p0(C,J)
| ~ n0(B,A)
| q1(J,A,J) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_092) ).
fof(f129_nnf,plain,
! [J,A,B,C] :
( ~ p0(C,J)
| ~ n0(B,A)
| q1(J,A,J) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [J,A,B,C] :
( ~ p0(C,J)
| ~ n0(B,A)
| q1(J,A,J) ),
inference(skolemisation,[status(esa)],[f129_nnf]) ).
cnf(c129,plain,
( ~ p0(X3,X0)
| ~ n0(X2,X1)
| q1(X0,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
cnf(hi127,axiom,
ifeq(n0(X0,X1),true,ifeq(p0(X2,X3),true,q1(X3,X1,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c129]) ).
cnf(f2,axiom,
n0(d,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_3) ).
fof(f2_nnf,plain,
n0(d,e),
inference(nnf_transformation,[status(thm)],[f2]) ).
cnf(c2,plain,
n0(d,e),
inference(cnf_transformation,[status(esa)],[f2_nnf]) ).
cnf(hi2,axiom,
n0(d,e) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h29,plain,
q1(V0,e,V0) = true,
inference(hyper_resolution,[status(thm)],[hi127,hi2,hi13]) ).
cnf(f206,axiom,
( ~ p1(D,F,D)
| ~ q1(E,E,E)
| p2(D,D,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_169) ).
fof(f206_nnf,plain,
! [D,E,F] :
( ~ p1(D,F,D)
| ~ q1(E,E,E)
| p2(D,D,D) ),
inference(nnf_transformation,[status(thm)],[f206]) ).
fof(f206_sk,plain,
! [D,E,F] :
( ~ p1(D,F,D)
| ~ q1(E,E,E)
| p2(D,D,D) ),
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c206,plain,
( ~ p1(X0,X2,X0)
| ~ q1(X1,X1,X1)
| p2(X0,X0,X0) ),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
cnf(hi203,axiom,
ifeq(q1(X0,X0,X0),true,ifeq(p1(X1,X2,X1),true,p2(X1,X1,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c206]) ).
cnf(h173,plain,
p2(V0,V0,V0) = true,
inference(hyper_resolution,[status(thm)],[hi203,h29,h30]) ).
cnf(f277,axiom,
( ~ p2(E,F,D)
| n3(D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_240) ).
fof(f277_nnf,plain,
! [D,E,F] :
( ~ p2(E,F,D)
| n3(D) ),
inference(nnf_transformation,[status(thm)],[f277]) ).
fof(f277_sk,plain,
! [D,E,F] :
( ~ p2(E,F,D)
| n3(D) ),
inference(skolemisation,[status(esa)],[f277_nnf]) ).
cnf(c277,plain,
( ~ p2(X1,X2,X0)
| n3(X0) ),
inference(cnf_transformation,[status(esa)],[f277_sk]) ).
cnf(hi272,axiom,
ifeq(p2(X0,X1,X2),true,n3(X2),true) = true,
inference(equality_encoding,[status(esa)],[c277]) ).
cnf(h339,plain,
n3(V0) = true,
inference(hyper_resolution,[status(thm)],[hi272,h173]) ).
cnf(f40,axiom,
( ~ m0(D,C,E)
| ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_003) ).
fof(f40_nnf,plain,
! [C,D,E,F] :
( ~ m0(D,C,E)
| ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [C,D,E,F] :
( ~ m0(D,C,E)
| ~ r0(F)
| ~ p0(E,C)
| l1(C,D) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( ~ m0(X1,X0,X2)
| ~ r0(X3)
| ~ p0(X2,X0)
| l1(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(hi40,axiom,
ifeq(p0(X0,X1),true,ifeq(r0(X2),true,ifeq(m0(X3,X1,X0),true,l1(X1,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c40]) ).
cnf(f17,axiom,
p0(c,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_18) ).
fof(f17_nnf,plain,
p0(c,b),
inference(nnf_transformation,[status(thm)],[f17]) ).
cnf(c17,plain,
p0(c,b),
inference(cnf_transformation,[status(esa)],[f17_nnf]) ).
cnf(hi17,axiom,
p0(c,b) = true,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(f12,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_13) ).
fof(f12_nnf,plain,
r0(e),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
r0(e),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(hi12,axiom,
r0(e) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(f26,axiom,
m0(e,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_27) ).
fof(f26_nnf,plain,
m0(e,b,c),
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
m0(e,b,c),
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(hi26,axiom,
m0(e,b,c) = true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(h87,plain,
l1(b,e) = true,
inference(hyper_resolution,[status(thm)],[hi40,hi17,hi12,hi26]) ).
cnf(f223,axiom,
( ~ l1(H,G)
| q2(G,G,H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_186) ).
fof(f223_nnf,plain,
! [G,H] :
( ~ l1(H,G)
| q2(G,G,H) ),
inference(nnf_transformation,[status(thm)],[f223]) ).
fof(f223_sk,plain,
! [G,H] :
( ~ l1(H,G)
| q2(G,G,H) ),
inference(skolemisation,[status(esa)],[f223_nnf]) ).
cnf(c223,plain,
( ~ l1(X1,X0)
| q2(X0,X0,X1) ),
inference(cnf_transformation,[status(esa)],[f223_sk]) ).
cnf(hi220,axiom,
ifeq(l1(X0,X1),true,q2(X1,X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c223]) ).
cnf(h242,plain,
q2(e,e,b) = true,
inference(hyper_resolution,[status(thm)],[hi220,h87]) ).
cnf(f292,axiom,
( ~ n0(I,G)
| ~ q2(I,G,H)
| q3(G,H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_255) ).
fof(f292_nnf,plain,
! [G,H,I] :
( ~ n0(I,G)
| ~ q2(I,G,H)
| q3(G,H) ),
inference(nnf_transformation,[status(thm)],[f292]) ).
fof(f292_sk,plain,
! [G,H,I] :
( ~ n0(I,G)
| ~ q2(I,G,H)
| q3(G,H) ),
inference(skolemisation,[status(esa)],[f292_nnf]) ).
cnf(c292,plain,
( ~ n0(X2,X0)
| ~ q2(X2,X0,X1)
| q3(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f292_sk]) ).
cnf(hi287,axiom,
ifeq(q2(X0,X1,X2),true,ifeq(n0(X0,X1),true,q3(X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c292]) ).
cnf(f29,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_30) ).
fof(f29_nnf,plain,
n0(e,e),
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
n0(e,e),
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(hi29,axiom,
n0(e,e) = true,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(h488,plain,
q3(e,b) = true,
inference(hyper_resolution,[status(thm)],[hi287,h242,hi29]) ).
cnf(f311,axiom,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_274) ).
fof(f311_nnf,plain,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
inference(nnf_transformation,[status(thm)],[f311]) ).
fof(f311_sk,plain,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
inference(skolemisation,[status(esa)],[f311_nnf]) ).
cnf(c311,plain,
( ~ n3(e)
| ~ q3(e,b)
| ~ n0(c,d)
| k4(c) ),
inference(cnf_transformation,[status(esa)],[f311_sk]) ).
cnf(hi306,axiom,
ifeq(n0(c,d),true,ifeq(q3(e,b),true,ifeq(n3(e),true,k4(c),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c311]) ).
cnf(f33,axiom,
n0(c,d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_34) ).
fof(f33_nnf,plain,
n0(c,d),
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
n0(c,d),
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(hi33,axiom,
n0(c,d) = true,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(h722,plain,
k4(c) = true,
inference(hyper_resolution,[status(thm)],[hi306,hi33,h488,h339]) ).
cnf(f321,axiom,
( ~ m3(H,H,H)
| ~ k4(I)
| n4(H,H) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_284) ).
fof(f321_nnf,plain,
! [H,I] :
( ~ m3(H,H,H)
| ~ k4(I)
| n4(H,H) ),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [H,I] :
( ~ m3(H,H,H)
| ~ k4(I)
| n4(H,H) ),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c321,plain,
( ~ m3(X0,X0,X0)
| ~ k4(X1)
| n4(X0,X0) ),
inference(cnf_transformation,[status(esa)],[f321_sk]) ).
cnf(hi314,axiom,
ifeq(k4(X0),true,ifeq(m3(X1,X1,X1),true,n4(X1,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c321]) ).
cnf(h729,plain,
n4(V0,V0) = true,
inference(hyper_resolution,[status(thm)],[hi314,h722,h219]) ).
cnf(f44,axiom,
( ~ r0(G)
| ~ p0(I,H)
| m1(G,H,G) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_007) ).
fof(f44_nnf,plain,
! [G,H,I] :
( ~ r0(G)
| ~ p0(I,H)
| m1(G,H,G) ),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [G,H,I] :
( ~ r0(G)
| ~ p0(I,H)
| m1(G,H,G) ),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c44,plain,
( ~ r0(X0)
| ~ p0(X2,X1)
| m1(X0,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
cnf(hi44,axiom,
ifeq(p0(X0,X1),true,ifeq(r0(X2),true,m1(X2,X1,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(h35,plain,
m1(e,V0,e) = true,
inference(hyper_resolution,[status(thm)],[hi44,hi13,hi12]) ).
cnf(f213,axiom,
( ~ m1(E,D,E)
| p2(D,E,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_176) ).
fof(f213_nnf,plain,
! [D,E] :
( ~ m1(E,D,E)
| p2(D,E,D) ),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [D,E] :
( ~ m1(E,D,E)
| p2(D,E,D) ),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c213,plain,
( ~ m1(X1,X0,X1)
| p2(X0,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
cnf(hi210,axiom,
ifeq(m1(X0,X1,X0),true,p2(X1,X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c213]) ).
cnf(h187,plain,
p2(V0,e,V0) = true,
inference(hyper_resolution,[status(thm)],[hi210,h35]) ).
cnf(f39,axiom,
( ~ n0(H,G)
| l1(G,G) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_002) ).
fof(f39_nnf,plain,
! [G,H] :
( ~ n0(H,G)
| l1(G,G) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [G,H] :
( ~ n0(H,G)
| l1(G,G) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c39,plain,
( ~ n0(X1,X0)
| l1(X0,X0) ),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
cnf(hi39,axiom,
ifeq(n0(X0,X1),true,l1(X1,X1),true) = true,
inference(equality_encoding,[status(esa)],[c39]) ).
cnf(f36,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_37) ).
fof(f36_nnf,plain,
n0(b,a),
inference(nnf_transformation,[status(thm)],[f36]) ).
cnf(c36,plain,
n0(b,a),
inference(cnf_transformation,[status(esa)],[f36_nnf]) ).
cnf(hi36,axiom,
n0(b,a) = true,
inference(equality_encoding,[status(esa)],[c36]) ).
cnf(h109,plain,
l1(a,a) = true,
inference(hyper_resolution,[status(thm)],[hi39,hi36]) ).
cnf(f119,axiom,
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| p1(H,I,J) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_082) ).
fof(f119_nnf,plain,
! [H,I,J,A] :
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| p1(H,I,J) ),
inference(nnf_transformation,[status(thm)],[f119]) ).
fof(f119_sk,plain,
! [H,I,J,A] :
( ~ p1(J,H,A)
| ~ m0(J,H,A)
| p1(H,I,J) ),
inference(skolemisation,[status(esa)],[f119_nnf]) ).
cnf(c119,plain,
( ~ p1(X2,X0,X3)
| ~ m0(X2,X0,X3)
| p1(X0,X1,X2) ),
inference(cnf_transformation,[status(esa)],[f119_sk]) ).
cnf(hi117,axiom,
ifeq(m0(X0,X1,X2),true,ifeq(p1(X0,X1,X2),true,p1(X1,X3,X0),true),true) = true,
inference(equality_encoding,[status(esa)],[c119]) ).
cnf(f11,axiom,
m0(a,X,a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_12) ).
fof(f11_nnf,plain,
! [X] : m0(a,X,a),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : m0(a,X,a),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
m0(a,X0,a),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi11,axiom,
m0(a,X0,a) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(h176,plain,
p1(a,V0,a) = true,
inference(hyper_resolution,[status(thm)],[hi117,hi11,h30]) ).
cnf(f183,axiom,
( ~ p2(C,D,C)
| ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_146) ).
fof(f183_nnf,plain,
! [C,D,E,F] :
( ~ p2(C,D,C)
| ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ),
inference(nnf_transformation,[status(thm)],[f183]) ).
fof(f183_sk,plain,
! [C,D,E,F] :
( ~ p2(C,D,C)
| ~ l1(E,F)
| ~ p1(C,E,F)
| p2(C,D,D) ),
inference(skolemisation,[status(esa)],[f183_nnf]) ).
cnf(c183,plain,
( ~ p2(X0,X1,X0)
| ~ l1(X2,X3)
| ~ p1(X0,X2,X3)
| p2(X0,X1,X1) ),
inference(cnf_transformation,[status(esa)],[f183_sk]) ).
cnf(hi180,axiom,
ifeq(p1(X0,X1,X2),true,ifeq(l1(X1,X2),true,ifeq(p2(X0,X3,X0),true,p2(X0,X3,X3),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c183]) ).
cnf(h352,plain,
p2(a,e,e) = true,
inference(hyper_resolution,[status(thm)],[hi180,h176,h109,h187]) ).
cnf(f288,axiom,
( ~ p2(A,B,D)
| ~ m3(B,C,D)
| p3(A,B,B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_251) ).
fof(f288_nnf,plain,
! [A,B,C,D] :
( ~ p2(A,B,D)
| ~ m3(B,C,D)
| p3(A,B,B) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [A,B,C,D] :
( ~ p2(A,B,D)
| ~ m3(B,C,D)
| p3(A,B,B) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
( ~ p2(X0,X1,X3)
| ~ m3(X1,X2,X3)
| p3(X0,X1,X1) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
cnf(hi283,axiom,
ifeq(m3(X0,X1,X2),true,ifeq(p2(X3,X0,X2),true,p3(X3,X0,X0),true),true) = true,
inference(equality_encoding,[status(esa)],[c288]) ).
cnf(h677,plain,
p3(a,e,e) = true,
inference(hyper_resolution,[status(thm)],[hi283,h219,h352]) ).
cnf(f318,axiom,
( ~ n4(J,J)
| ~ p3(J,A,A)
| n4(J,A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rule_281) ).
fof(f318_nnf,plain,
! [J,A] :
( ~ n4(J,J)
| ~ p3(J,A,A)
| n4(J,A) ),
inference(nnf_transformation,[status(thm)],[f318]) ).
fof(f318_sk,plain,
! [J,A] :
( ~ n4(J,J)
| ~ p3(J,A,A)
| n4(J,A) ),
inference(skolemisation,[status(esa)],[f318_nnf]) ).
cnf(c318,plain,
( ~ n4(X0,X0)
| ~ p3(X0,X1,X1)
| n4(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f318_sk]) ).
cnf(hi311,axiom,
ifeq(p3(X0,X1,X1),true,ifeq(n4(X0,X0),true,n4(X0,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c318]) ).
cnf(t73,plain,
n4(a,e) = true,
inference(hyper_resolution,[status(thm)],[hi311,h677,h729]) ).
cnf(t511,plain,
n4(a,e) = true,
inference(orient,[status(thm)],[t73]) ).
cnf(f368,negated_conjecture,
~ n4(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
fof(f368_nnf,plain,
~ n4(a,e),
inference(nnf_transformation,[status(thm)],[f368]) ).
fof(f368_sk,plain,
~ n4(a,e),
inference(skolemisation,[status(esa)],[f368_nnf]) ).
cnf(c368,plain,
~ n4(a,e),
inference(cnf_transformation,[status(esa)],[f368_sk]) ).
cnf(goal_0,negated_conjecture,
n4(a,e) != true,
inference(equality_encoding,[status(esa)],[c368]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t511]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN156-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Fri Sep 25 00:20:33 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 8.73/1.73 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.73/1.73 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------