%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SYN067-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Thu Sep 24 03:15:07 PM UTC 2026
% Result : Unsatisfiable 0.09s 0.61s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 5
% Number of leaves : 84
% Syntax : Number of formulae : 313 ( 1 unt; 37 def)
% Number of atoms : 1300 ( 0 equ)
% Maximal formula atoms : 9 ( 4 avg)
% Number of connectives : 1695 ( 708 ~; 950 |; 0 &)
% ( 37 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 40 ( 39 usr; 38 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 5 con; 0-1 aty)
% Number of variables : 473 ( 473 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,negated_conjecture,
! [B,D,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_r(sk2(B),sk1(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,negated_conjecture,
! [B,D,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_r(B,sk2(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,negated_conjecture,
! [D,B,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk2(B),sk1(B))
| big_r(D,sk6(D)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f4,negated_conjecture,
! [D,B,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(B,sk2(B))
| big_r(D,sk6(D)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f5,negated_conjecture,
! [B,D,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_p(sk1(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,negated_conjecture,
! [B,D,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(D,sk6(D))
| big_p(sk1(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,negated_conjecture,
! [D,B,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk2(B),sk1(B))
| big_p(sk5(D)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,negated_conjecture,
! [D,B,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(B,sk2(B))
| big_p(sk5(D)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,negated_conjecture,
! [B,D,C,A] :
( ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk5(D))
| big_p(sk1(B)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,negated_conjecture,
! [A,C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| big_r(sk2(A),sk1(A))
| big_p(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,negated_conjecture,
! [A,C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| big_r(A,sk2(A))
| big_p(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f16,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk4(C),sk3(C))
| big_r(sk2(B),sk1(B))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk4(C),sk3(C))
| big_r(B,sk2(B))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk2(B),sk1(B))
| big_r(C,sk4(C))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f20,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk4(C),sk3(C))
| big_p(sk1(B))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f21,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(C,sk4(C))
| big_p(sk1(B))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk2(B),sk1(B))
| big_p(sk3(C))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(B,sk2(B))
| big_p(sk3(C))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f24,negated_conjecture,
! [C,B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_p(sk3(C))
| big_p(sk1(B))
| big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f25,negated_conjecture,
! [B,A] :
( big_r(sk4(B),sk3(B))
| big_r(sk2(A),sk1(A))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,negated_conjecture,
! [B,A] :
( big_r(sk2(A),sk1(A))
| big_r(B,sk4(B))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,negated_conjecture,
! [B,A] :
( big_r(sk4(B),sk3(B))
| big_r(A,sk2(A))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,negated_conjecture,
! [B,A] :
( big_r(A,sk2(A))
| big_r(B,sk4(B))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
! [B,A] :
( big_r(sk2(A),sk1(A))
| big_p(sk3(B))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
! [B,A] :
( big_r(A,sk2(A))
| big_p(sk3(B))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
! [A,C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| big_p(sk1(A))
| big_p(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
! [B,A] :
( big_r(sk4(B),sk3(B))
| big_p(sk1(A))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
! [B,A] :
( big_r(B,sk4(B))
| big_p(sk1(A))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
! [B,A] :
( big_p(sk3(B))
| big_p(sk1(A))
| big_p(A)
| big_p(B) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_p(sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk10,sk11)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,negated_conjecture,
! [A,B] :
( ~ big_r(sk10,B)
| ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(A)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,negated_conjecture,
! [A,B] :
( ~ big_r(sk9,B)
| ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_p(sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,negated_conjecture,
! [A,B] :
( ~ big_r(sk9,B)
| ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk10,sk11)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,negated_conjecture,
! [C,A,D,B] :
( ~ big_r(sk9,B)
| ~ big_r(sk10,D)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(sk7)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,negated_conjecture,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
! [A,B] :
( ~ big_r(sk10,B)
| ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f47,negated_conjecture,
! [A,B] :
( ~ big_r(sk9,B)
| ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f48,negated_conjecture,
! [A,B] :
( ~ big_r(sk9,B)
| ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,negated_conjecture,
! [C,A,D,B] :
( ~ big_r(sk9,B)
| ~ big_r(sk10,D)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(sk7)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk7,sk8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f50,negated_conjecture,
! [A,B] :
( ~ big_r(sk7,B)
| ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(A)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,negated_conjecture,
! [A,B] :
( ~ big_r(sk7,B)
| ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(A)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f52,negated_conjecture,
! [C,A,D,B] :
( ~ big_r(sk7,B)
| ~ big_r(sk10,D)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(sk9)
| ~ big_p(A)
| ~ big_p(C) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f53,negated_conjecture,
! [C,A,D,B] :
( ~ big_r(sk9,D)
| ~ big_r(sk7,B)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
! [C,A,D,B] :
( ~ big_r(sk9,D)
| ~ big_r(sk7,B)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk10,sk11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,negated_conjecture,
! [E,C,A,F,D,B] :
( ~ big_r(sk9,D)
| ~ big_r(sk7,B)
| ~ big_r(sk10,F)
| ~ big_r(B,A)
| ~ big_r(D,C)
| ~ big_r(F,E)
| ~ big_p(A)
| ~ big_p(C)
| ~ big_p(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f56,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_r(sk2(B),sk1(B)) ) ),
inference(miniscoping,[status(thm)],[f1]) ).
fof(f57,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(sk2(X0),sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f56]) ).
fof(f58,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_r(B,sk2(B)) ) ),
inference(miniscoping,[status(thm)],[f2]) ).
fof(f59,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(X0,sk2(X0)) ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f60,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk2(B),sk1(B))
| big_r(D,sk6(D)) ) ),
inference(miniscoping,[status(thm)],[f3]) ).
fof(f61,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk6(X0)) ),
inference(cnf_transformation,[status(thm)],[f60]) ).
fof(f62,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(B,sk2(B))
| big_r(D,sk6(D)) ) ),
inference(miniscoping,[status(thm)],[f4]) ).
fof(f63,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_r(X0,sk6(X0)) ),
inference(cnf_transformation,[status(thm)],[f62]) ).
fof(f64,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk6(D),sk5(D))
| big_p(sk1(B)) ) ),
inference(miniscoping,[status(thm)],[f5]) ).
fof(f65,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f64]) ).
fof(f66,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(D,sk6(D))
| big_p(sk1(B)) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f67,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk6(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f66]) ).
fof(f68,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk2(B),sk1(B))
| big_p(sk5(D)) ) ),
inference(miniscoping,[status(thm)],[f7]) ).
fof(f69,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_p(sk5(X0)) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f70,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(B,sk2(B))
| big_p(sk5(D)) ) ),
inference(miniscoping,[status(thm)],[f8]) ).
fof(f71,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X1,X3)
| ~ big_r(X0,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_p(sk5(X0)) ),
inference(cnf_transformation,[status(thm)],[f70]) ).
fof(f72,plain,
! [B,A] :
( ~ big_r(B,A)
| ! [D,C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk5(D))
| big_p(sk1(B)) ) ),
inference(miniscoping,[status(thm)],[f9]) ).
fof(f73,plain,
! [X0,X1,X2,X3] :
( ~ big_r(X0,X3)
| ~ big_r(X1,X2)
| ~ big_p(X3)
| ~ big_p(X2)
| big_p(sk5(X1))
| big_p(sk1(X0)) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f74,plain,
! [C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| ! [A] :
( big_r(sk2(A),sk1(A))
| big_p(A) ) ),
inference(miniscoping,[status(thm)],[f10]) ).
fof(f75,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(sk2(X0),sk1(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f78,plain,
! [C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| ! [A] :
( big_r(A,sk2(A))
| big_p(A) ) ),
inference(miniscoping,[status(thm)],[f12]) ).
fof(f79,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_r(X0,sk2(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f86,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| ! [C] :
( big_r(sk4(C),sk3(C))
| big_r(sk2(B),sk1(B))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f16]) ).
fof(f87,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_r(sk2(X1),sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f88,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| ! [C] :
( big_r(sk4(C),sk3(C))
| big_r(B,sk2(B))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f17]) ).
fof(f89,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_r(X1,sk2(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f88]) ).
fof(f90,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk2(B),sk1(B))
| ! [C] :
( big_r(C,sk4(C))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f18]) ).
fof(f91,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f94,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| ! [C] :
( big_r(sk4(C),sk3(C))
| big_p(sk1(B))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f20]) ).
fof(f95,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk4(X0),sk3(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f96,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| ! [C] :
( big_r(C,sk4(C))
| big_p(sk1(B))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f21]) ).
fof(f97,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f96]) ).
fof(f98,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(sk2(B),sk1(B))
| ! [C] :
( big_p(sk3(C))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f22]) ).
fof(f99,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk2(X1),sk1(X1))
| big_p(sk3(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f100,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| big_r(B,sk2(B))
| ! [C] :
( big_p(sk3(C))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f101,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(X1,sk2(X1))
| big_p(sk3(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f100]) ).
fof(f102,plain,
! [B,A] :
( ~ big_r(B,A)
| ~ big_p(A)
| ! [C] :
( big_p(sk3(C))
| big_p(sk1(B))
| big_p(C) ) ),
inference(miniscoping,[status(thm)],[f24]) ).
fof(f103,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f104,plain,
! [B] :
( big_r(sk4(B),sk3(B))
| ! [A] :
( big_r(sk2(A),sk1(A))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f105,plain,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_r(sk2(X1),sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f104]) ).
fof(f106,plain,
! [A] :
( big_r(sk2(A),sk1(A))
| ! [B] :
( big_r(B,sk4(B))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f26]) ).
fof(f107,plain,
! [X0,X1] :
( big_r(sk2(X1),sk1(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f108,plain,
! [B] :
( big_r(sk4(B),sk3(B))
| ! [A] :
( big_r(A,sk2(A))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f27]) ).
fof(f109,plain,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_r(X1,sk2(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f108]) ).
fof(f110,plain,
! [A] :
( big_r(A,sk2(A))
| ! [B] :
( big_r(B,sk4(B))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f28]) ).
fof(f111,plain,
! [X0,X1] :
( big_r(X1,sk2(X1))
| big_r(X0,sk4(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f110]) ).
fof(f112,plain,
! [A] :
( big_r(sk2(A),sk1(A))
| ! [B] :
( big_p(sk3(B))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f29]) ).
fof(f113,plain,
! [X0,X1] :
( big_r(sk2(X1),sk1(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f112]) ).
fof(f114,plain,
! [A] :
( big_r(A,sk2(A))
| ! [B] :
( big_p(sk3(B))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f30]) ).
fof(f115,plain,
! [X0,X1] :
( big_r(X1,sk2(X1))
| big_p(sk3(X0))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f114]) ).
fof(f116,plain,
! [C,B] :
( ~ big_r(C,B)
| ~ big_p(B)
| big_r(sk6(C),sk5(C))
| ! [A] :
( big_p(sk1(A))
| big_p(A) ) ),
inference(miniscoping,[status(thm)],[f31]) ).
fof(f117,plain,
! [X0,X1,X2] :
( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1))
| big_p(sk1(X0))
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f116]) ).
fof(f122,plain,
! [B] :
( big_r(sk4(B),sk3(B))
| ! [A] :
( big_p(sk1(A))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f34]) ).
fof(f123,plain,
! [X0,X1] :
( big_r(sk4(X0),sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f122]) ).
fof(f124,plain,
! [B] :
( big_r(B,sk4(B))
| ! [A] :
( big_p(sk1(A))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f35]) ).
fof(f125,plain,
! [X0,X1] :
( big_r(X0,sk4(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f124]) ).
fof(f126,plain,
! [B] :
( big_p(sk3(B))
| ! [A] :
( big_p(sk1(A))
| big_p(A)
| big_p(B) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f127,plain,
! [X0,X1] :
( big_p(sk3(X0))
| big_p(sk1(X1))
| big_p(X1)
| big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f126]) ).
fof(f129,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_p(sk8)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f130,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk10,sk11)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f131,plain,
! [B] :
( ~ big_r(sk10,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(A)
| big_p(sk8) ) ),
inference(miniscoping,[status(thm)],[f40]) ).
fof(f132,plain,
! [X0,X1] :
( ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f131]) ).
fof(f133,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_p(sk8)
| big_p(sk11) ) ),
inference(miniscoping,[status(thm)],[f41]) ).
fof(f134,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_p(sk8)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f133]) ).
fof(f135,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk10,sk11)
| big_p(sk8) ) ),
inference(miniscoping,[status(thm)],[f42]) ).
fof(f136,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk10,sk11)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f135]) ).
fof(f137,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [D] :
( ~ big_r(sk10,D)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ~ big_p(sk7)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk8) ) ) ) ),
inference(miniscoping,[status(thm)],[f43]) ).
fof(f138,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk9,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_p(X0)
| big_p(sk8) ),
inference(cnf_transformation,[status(thm)],[f137]) ).
fof(f139,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f140,plain,
( ~ big_p(sk9)
| ~ big_p(sk7)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f141,plain,
! [B] :
( ~ big_r(sk10,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8) ) ),
inference(miniscoping,[status(thm)],[f46]) ).
fof(f142,plain,
! [X0,X1] :
( ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8) ),
inference(cnf_transformation,[status(thm)],[f141]) ).
fof(f143,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8)
| big_p(sk11) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f144,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f145,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk7)
| ~ big_p(A)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ) ),
inference(miniscoping,[status(thm)],[f48]) ).
fof(f146,plain,
! [X0,X1] :
( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk7)
| ~ big_p(X0)
| big_r(sk7,sk8)
| big_r(sk10,sk11) ),
inference(cnf_transformation,[status(thm)],[f145]) ).
fof(f147,plain,
! [B] :
( ~ big_r(sk9,B)
| ! [D] :
( ~ big_r(sk10,D)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ~ big_p(sk7)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk7,sk8) ) ) ) ),
inference(miniscoping,[status(thm)],[f49]) ).
fof(f148,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk9,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk7)
| ~ big_p(X1)
| ~ big_p(X0)
| big_r(sk7,sk8) ),
inference(cnf_transformation,[status(thm)],[f147]) ).
fof(f149,plain,
! [B] :
( ~ big_r(sk7,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(A)
| big_p(sk11) ) ),
inference(miniscoping,[status(thm)],[f50]) ).
fof(f150,plain,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f149]) ).
fof(f151,plain,
! [B] :
( ~ big_r(sk7,B)
| ! [A] :
( ~ big_r(B,A)
| ~ big_p(sk9)
| ~ big_p(A)
| big_r(sk10,sk11) ) ),
inference(miniscoping,[status(thm)],[f51]) ).
fof(f152,plain,
! [X0,X1] :
( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(sk9)
| ~ big_p(X0)
| big_r(sk10,sk11) ),
inference(cnf_transformation,[status(thm)],[f151]) ).
fof(f153,plain,
! [B] :
( ~ big_r(sk7,B)
| ! [D] :
( ~ big_r(sk10,D)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ~ big_p(sk9)
| ~ big_p(A)
| ~ big_p(C) ) ) ) ),
inference(miniscoping,[status(thm)],[f52]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk7,X3)
| ~ big_r(sk10,X2)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(sk9)
| ~ big_p(X1)
| ~ big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f153]) ).
fof(f155,plain,
! [D] :
( ~ big_r(sk9,D)
| ! [B] :
( ~ big_r(sk7,B)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_p(sk11) ) ) ) ),
inference(miniscoping,[status(thm)],[f53]) ).
fof(f156,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk9,X2)
| ~ big_r(sk7,X3)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(X1)
| ~ big_p(X0)
| big_p(sk11) ),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [D] :
( ~ big_r(sk9,D)
| ! [B] :
( ~ big_r(sk7,B)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ~ big_p(A)
| ~ big_p(C)
| big_r(sk10,sk11) ) ) ) ),
inference(miniscoping,[status(thm)],[f54]) ).
fof(f158,plain,
! [X0,X1,X2,X3] :
( ~ big_r(sk9,X2)
| ~ big_r(sk7,X3)
| ~ big_r(X3,X1)
| ~ big_r(X2,X0)
| ~ big_p(X1)
| ~ big_p(X0)
| big_r(sk10,sk11) ),
inference(cnf_transformation,[status(thm)],[f157]) ).
fof(f159,plain,
! [D] :
( ~ big_r(sk9,D)
| ! [B] :
( ~ big_r(sk7,B)
| ! [F] :
( ~ big_r(sk10,F)
| ! [A] :
( ~ big_r(B,A)
| ! [C] :
( ~ big_r(D,C)
| ! [E] :
( ~ big_r(F,E)
| ~ big_p(A)
| ~ big_p(C)
| ~ big_p(E) ) ) ) ) ) ),
inference(miniscoping,[status(thm)],[f55]) ).
fof(f160,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ big_r(sk9,X4)
| ~ big_r(sk7,X5)
| ~ big_r(sk10,X3)
| ~ big_r(X5,X2)
| ~ big_r(X4,X1)
| ~ big_r(X3,X0)
| ~ big_p(X2)
| ~ big_p(X1)
| ~ big_p(X0) ),
inference(cnf_transformation,[status(thm)],[f159]) ).
fof(f161,definition,
! [X0,X3] :
( sQ0_spl
<=> ( ~ big_r(X0,X3)
| ~ big_p(X3)
| big_r(sk2(X0),sk1(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f162,plain,
! [X0,X1] :
( ~ sQ0_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(sk2(X0),sk1(X0)) ),
inference(component_clause,[status(thm)],[f161]) ).
fof(f164,definition,
! [X1,X2] :
( sQ1_spl
<=> ( ~ big_r(X1,X2)
| ~ big_p(X2)
| big_r(sk6(X1),sk5(X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f165,plain,
! [X0,X1] :
( ~ sQ1_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(sk6(X0),sk5(X0)) ),
inference(component_clause,[status(thm)],[f164]) ).
fof(f167,plain,
( sQ1_spl
| sQ0_spl ),
inference(split_clause,[status(thm)],[f57,f161,f164]) ).
fof(f168,definition,
! [X0,X3] :
( sQ2_spl
<=> ( ~ big_r(X0,X3)
| ~ big_p(X3)
| big_r(X0,sk2(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f169,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(X0,sk2(X0)) ),
inference(component_clause,[status(thm)],[f168]) ).
fof(f171,plain,
( sQ1_spl
| sQ2_spl ),
inference(split_clause,[status(thm)],[f59,f168,f164]) ).
fof(f172,definition,
! [X0,X2] :
( sQ3_spl
<=> ( ~ big_r(X0,X2)
| ~ big_p(X2)
| big_r(X0,sk6(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f173,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_r(X0,sk6(X0)) ),
inference(component_clause,[status(thm)],[f172]) ).
fof(f175,plain,
( sQ0_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f61,f172,f161]) ).
fof(f176,plain,
( sQ2_spl
| sQ3_spl ),
inference(split_clause,[status(thm)],[f63,f172,f168]) ).
fof(f177,definition,
! [X0,X3] :
( sQ4_spl
<=> ( ~ big_r(X0,X3)
| ~ big_p(X3)
| big_p(sk1(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f178,plain,
! [X0,X1] :
( ~ sQ4_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_p(sk1(X0)) ),
inference(component_clause,[status(thm)],[f177]) ).
fof(f180,plain,
( sQ1_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f65,f177,f164]) ).
fof(f181,plain,
( sQ3_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f67,f177,f172]) ).
fof(f182,definition,
! [X0,X2] :
( sQ5_spl
<=> ( ~ big_r(X0,X2)
| ~ big_p(X2)
| big_p(sk5(X0)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f183,plain,
! [X0,X1] :
( ~ sQ5_spl
| ~ big_r(X0,X1)
| ~ big_p(X1)
| big_p(sk5(X0)) ),
inference(component_clause,[status(thm)],[f182]) ).
fof(f185,plain,
( sQ0_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f69,f182,f161]) ).
fof(f186,plain,
( sQ2_spl
| sQ5_spl ),
inference(split_clause,[status(thm)],[f71,f182,f168]) ).
fof(f187,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f73,f177,f182]) ).
fof(f188,definition,
! [X0] :
( sQ6_spl
<=> ( big_r(sk2(X0),sk1(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f189,plain,
! [X0] :
( ~ sQ6_spl
| big_r(sk2(X0),sk1(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f188]) ).
fof(f191,plain,
( sQ1_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f75,f188,f164]) ).
fof(f193,definition,
! [X0] :
( sQ7_spl
<=> ( big_r(X0,sk2(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f194,plain,
! [X0] :
( ~ sQ7_spl
| big_r(X0,sk2(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f193]) ).
fof(f196,plain,
( sQ1_spl
| sQ7_spl ),
inference(split_clause,[status(thm)],[f79,f193,f164]) ).
fof(f200,definition,
! [X0] :
( sQ8_spl
<=> ( big_r(sk4(X0),sk3(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f201,plain,
! [X0] :
( ~ sQ8_spl
| big_r(sk4(X0),sk3(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f200]) ).
fof(f203,plain,
( sQ0_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f87,f200,f161]) ).
fof(f204,plain,
( sQ2_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f89,f200,f168]) ).
fof(f205,definition,
! [X0] :
( sQ9_spl
<=> ( big_r(X0,sk4(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f206,plain,
! [X0] :
( ~ sQ9_spl
| big_r(X0,sk4(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f205]) ).
fof(f208,plain,
( sQ0_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f91,f205,f161]) ).
fof(f210,plain,
( sQ4_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f95,f200,f177]) ).
fof(f211,plain,
( sQ4_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f97,f205,f177]) ).
fof(f212,definition,
! [X0] :
( sQ10_spl
<=> ( big_p(sk3(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f213,plain,
! [X0] :
( ~ sQ10_spl
| big_p(sk3(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f212]) ).
fof(f215,plain,
( sQ0_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f99,f212,f161]) ).
fof(f216,plain,
( sQ2_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f101,f212,f168]) ).
fof(f217,plain,
( sQ4_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f103,f212,f177]) ).
fof(f218,plain,
( sQ6_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f105,f200,f188]) ).
fof(f219,plain,
( sQ6_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f107,f205,f188]) ).
fof(f220,plain,
( sQ7_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f109,f200,f193]) ).
fof(f221,plain,
( sQ7_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f111,f205,f193]) ).
fof(f222,plain,
( sQ6_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f113,f212,f188]) ).
fof(f223,plain,
( sQ7_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f115,f212,f193]) ).
fof(f224,definition,
! [X0] :
( sQ11_spl
<=> ( big_p(sk1(X0))
| big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f225,plain,
! [X0] :
( ~ sQ11_spl
| big_p(sk1(X0))
| big_p(X0) ),
inference(component_clause,[status(thm)],[f224]) ).
fof(f227,plain,
( sQ1_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f117,f224,f164]) ).
fof(f230,plain,
( sQ11_spl
| sQ8_spl ),
inference(split_clause,[status(thm)],[f123,f200,f224]) ).
fof(f231,plain,
( sQ11_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f125,f205,f224]) ).
fof(f232,plain,
( sQ11_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f127,f212,f224]) ).
fof(f233,definition,
( sQ12_spl
<=> big_p(sk11) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f234,plain,
( ~ sQ12_spl
| big_p(sk11) ),
inference(component_clause,[status(thm)],[f233]) ).
fof(f236,definition,
( sQ13_spl
<=> big_p(sk8) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f237,plain,
( ~ sQ13_spl
| big_p(sk8) ),
inference(component_clause,[status(thm)],[f236]) ).
fof(f239,definition,
( sQ14_spl
<=> big_p(sk7) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f241,plain,
( sQ14_spl
| ~ big_p(sk7) ),
inference(component_clause,[status(thm)],[f239]) ).
fof(f242,definition,
( sQ15_spl
<=> big_p(sk9) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f245,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f129,f233,f236,f239,f242]) ).
fof(f246,definition,
( sQ16_spl
<=> big_r(sk10,sk11) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f247,plain,
( ~ sQ16_spl
| big_r(sk10,sk11) ),
inference(component_clause,[status(thm)],[f246]) ).
fof(f249,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ16_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f130,f236,f246,f239,f242]) ).
fof(f250,definition,
! [X0,X1] :
( sQ17_spl
<=> ( ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f251,plain,
! [X0,X1] :
( ~ sQ17_spl
| ~ big_r(sk10,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f250]) ).
fof(f253,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ17_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f132,f236,f250,f239,f242]) ).
fof(f254,definition,
! [X0,X1] :
( sQ18_spl
<=> ( ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f255,plain,
! [X0,X1] :
( ~ sQ18_spl
| ~ big_r(sk9,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f254]) ).
fof(f257,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ13_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f134,f233,f236,f254,f239]) ).
fof(f258,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ16_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f136,f236,f246,f254,f239]) ).
fof(f259,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ17_spl
| sQ13_spl ),
inference(split_clause,[status(thm)],[f138,f236,f250,f254,f239]) ).
fof(f260,definition,
( sQ19_spl
<=> big_r(sk7,sk8) ),
introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition]) ).
fof(f261,plain,
( ~ sQ19_spl
| big_r(sk7,sk8) ),
inference(component_clause,[status(thm)],[f260]) ).
fof(f263,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ19_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f139,f233,f260,f239,f242]) ).
fof(f264,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ19_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f140,f246,f260,f239,f242]) ).
fof(f265,plain,
( ~ sQ15_spl
| ~ sQ14_spl
| sQ17_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f142,f260,f250,f239,f242]) ).
fof(f266,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ19_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f144,f233,f260,f254,f239]) ).
fof(f267,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ19_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f146,f246,f260,f254,f239]) ).
fof(f268,plain,
( ~ sQ14_spl
| sQ18_spl
| sQ17_spl
| sQ19_spl ),
inference(split_clause,[status(thm)],[f148,f260,f250,f254,f239]) ).
fof(f269,definition,
! [X0,X1] :
( sQ20_spl
<=> ( ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition]) ).
fof(f270,plain,
! [X0,X1] :
( ~ sQ20_spl
| ~ big_r(sk7,X1)
| ~ big_r(X1,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f269]) ).
fof(f272,plain,
( ~ sQ15_spl
| sQ20_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f150,f233,f269,f242]) ).
fof(f273,plain,
( ~ sQ15_spl
| sQ20_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f152,f246,f269,f242]) ).
fof(f274,plain,
( ~ sQ15_spl
| sQ20_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f154,f250,f269,f242]) ).
fof(f275,plain,
( sQ20_spl
| sQ18_spl
| sQ12_spl ),
inference(split_clause,[status(thm)],[f156,f233,f254,f269]) ).
fof(f276,plain,
( sQ20_spl
| sQ18_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f158,f246,f254,f269]) ).
fof(f277,plain,
( sQ20_spl
| sQ18_spl
| sQ17_spl ),
inference(split_clause,[status(thm)],[f160,f250,f254,f269]) ).
fof(f278,plain,
! [X0] :
( ~ sQ18_spl
| ~ sQ9_spl
| ~ big_r(sk4(sk9),X0)
| ~ big_p(X0)
| big_p(sk9) ),
inference(resolution,[status(thm)],[f206,f255]) ).
fof(f279,definition,
! [X0] :
( sQ21_spl
<=> ( ~ big_r(sk4(sk9),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f280,plain,
! [X0] :
( ~ sQ21_spl
| ~ big_r(sk4(sk9),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f279]) ).
fof(f282,plain,
( ~ sQ18_spl
| ~ sQ9_spl
| sQ21_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f278,f242,f279,f205,f254]) ).
fof(f283,plain,
( ~ sQ8_spl
| ~ sQ21_spl
| big_p(sk9)
| ~ big_p(sk3(sk9)) ),
inference(resolution,[status(thm)],[f280,f201]) ).
fof(f285,definition,
( sQ22_spl
<=> big_p(sk3(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f287,plain,
( sQ22_spl
| ~ big_p(sk3(sk9)) ),
inference(component_clause,[status(thm)],[f285]) ).
fof(f288,plain,
( ~ sQ8_spl
| ~ sQ21_spl
| sQ15_spl
| ~ sQ22_spl ),
inference(split_clause,[status(thm)],[f283,f285,f242,f279,f200]) ).
fof(f296,plain,
( ~ sQ10_spl
| sQ22_spl
| big_p(sk9) ),
inference(resolution,[status(thm)],[f287,f213]) ).
fof(f298,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ20_spl
| ~ big_r(sk7,X1)
| ~ big_p(X1)
| ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f270,f169]) ).
fof(f299,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ20_spl
| ~ big_r(sk7,X1)
| ~ big_p(X1)
| ~ big_r(sk6(sk7),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f270,f173]) ).
fof(f300,plain,
! [X0] :
( ~ sQ9_spl
| ~ sQ20_spl
| big_p(sk7)
| ~ big_r(sk4(sk7),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f270,f206]) ).
fof(f301,definition,
! [X0] :
( sQ25_spl
<=> ( ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition]) ).
fof(f302,plain,
! [X0] :
( ~ sQ25_spl
| ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f301]) ).
fof(f304,definition,
! [X1] :
( sQ26_spl
<=> ( ~ big_r(sk7,X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition]) ).
fof(f305,plain,
! [X0] :
( ~ sQ26_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f304]) ).
fof(f307,plain,
( ~ sQ2_spl
| ~ sQ20_spl
| sQ26_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f298,f301,f304,f269,f168]) ).
fof(f308,definition,
! [X0] :
( sQ27_spl
<=> ( ~ big_r(sk6(sk7),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition]) ).
fof(f309,plain,
! [X0] :
( ~ sQ27_spl
| ~ big_r(sk6(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f308]) ).
fof(f311,plain,
( ~ sQ3_spl
| ~ sQ20_spl
| sQ26_spl
| sQ27_spl ),
inference(split_clause,[status(thm)],[f299,f308,f304,f269,f172]) ).
fof(f312,definition,
! [X0] :
( sQ28_spl
<=> ( ~ big_r(sk4(sk7),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition]) ).
fof(f313,plain,
! [X0] :
( ~ sQ28_spl
| ~ big_r(sk4(sk7),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f312]) ).
fof(f315,plain,
( ~ sQ9_spl
| ~ sQ20_spl
| sQ14_spl
| sQ28_spl ),
inference(split_clause,[status(thm)],[f300,f312,f239,f269,f205]) ).
fof(f316,plain,
( ~ sQ10_spl
| sQ22_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f296,f242,f285,f212]) ).
fof(f317,plain,
( ~ sQ19_spl
| ~ sQ26_spl
| ~ big_p(sk8) ),
inference(resolution,[status(thm)],[f305,f261]) ).
fof(f320,plain,
( ~ sQ19_spl
| ~ sQ26_spl
| ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f317,f237]) ).
fof(f321,plain,
( ~ sQ19_spl
| ~ sQ26_spl
| ~ sQ13_spl ),
inference(contradiction_clause,[status(thm)],[f320]) ).
fof(f322,plain,
( ~ sQ8_spl
| ~ sQ28_spl
| big_p(sk7)
| ~ big_p(sk3(sk7)) ),
inference(resolution,[status(thm)],[f313,f201]) ).
fof(f326,definition,
( sQ29_spl
<=> big_p(sk3(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f328,plain,
( sQ29_spl
| ~ big_p(sk3(sk7)) ),
inference(component_clause,[status(thm)],[f326]) ).
fof(f329,plain,
( ~ sQ8_spl
| ~ sQ28_spl
| sQ14_spl
| ~ sQ29_spl ),
inference(split_clause,[status(thm)],[f322,f326,f239,f312,f200]) ).
fof(f343,plain,
! [X0,X1] :
( ~ sQ2_spl
| ~ sQ17_spl
| ~ big_r(sk10,X1)
| ~ big_p(X1)
| ~ big_r(sk2(sk10),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f251,f169]) ).
fof(f344,plain,
! [X0,X1] :
( ~ sQ3_spl
| ~ sQ17_spl
| ~ big_r(sk10,X1)
| ~ big_p(X1)
| ~ big_r(sk6(sk10),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f251,f173]) ).
fof(f345,definition,
! [X0] :
( sQ33_spl
<=> ( ~ big_r(sk2(sk10),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f346,plain,
! [X0] :
( ~ sQ33_spl
| ~ big_r(sk2(sk10),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f345]) ).
fof(f348,definition,
! [X1] :
( sQ34_spl
<=> ( ~ big_r(sk10,X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition]) ).
fof(f349,plain,
! [X0] :
( ~ sQ34_spl
| ~ big_r(sk10,X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f348]) ).
fof(f351,plain,
( ~ sQ2_spl
| ~ sQ17_spl
| sQ34_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f343,f345,f348,f250,f168]) ).
fof(f352,definition,
! [X0] :
( sQ35_spl
<=> ( ~ big_r(sk6(sk10),X0)
| ~ big_p(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition]) ).
fof(f353,plain,
! [X0] :
( ~ sQ35_spl
| ~ big_r(sk6(sk10),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f352]) ).
fof(f355,plain,
( ~ sQ3_spl
| ~ sQ17_spl
| sQ34_spl
| sQ35_spl ),
inference(split_clause,[status(thm)],[f344,f352,f348,f250,f172]) ).
fof(f356,plain,
( ~ sQ10_spl
| sQ29_spl
| big_p(sk7) ),
inference(resolution,[status(thm)],[f328,f213]) ).
fof(f357,plain,
( ~ sQ10_spl
| sQ29_spl
| sQ14_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f356,f241]) ).
fof(f358,plain,
( ~ sQ10_spl
| sQ29_spl
| sQ14_spl ),
inference(contradiction_clause,[status(thm)],[f357]) ).
fof(f367,plain,
( ~ sQ16_spl
| ~ sQ34_spl
| ~ big_p(sk11) ),
inference(resolution,[status(thm)],[f349,f247]) ).
fof(f368,plain,
( ~ sQ16_spl
| ~ sQ34_spl
| ~ sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f367,f234]) ).
fof(f369,plain,
( ~ sQ16_spl
| ~ sQ34_spl
| ~ sQ12_spl ),
inference(contradiction_clause,[status(thm)],[f368]) ).
fof(f374,definition,
! [X1] :
( sQ39_spl
<=> ( ~ big_r(sk2(sk9),X1)
| ~ big_p(X1) ) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f375,plain,
! [X0] :
( ~ sQ39_spl
| ~ big_r(sk2(sk9),X0)
| ~ big_p(X0) ),
inference(component_clause,[status(thm)],[f374]) ).
fof(f378,plain,
! [X0] :
( ~ sQ18_spl
| ~ sQ7_spl
| ~ big_r(sk2(sk9),X0)
| ~ big_p(X0)
| big_p(sk9) ),
inference(resolution,[status(thm)],[f194,f255]) ).
fof(f379,plain,
( ~ sQ18_spl
| ~ sQ7_spl
| sQ39_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f378,f242,f374,f193,f254]) ).
fof(f397,plain,
! [X0] :
( ~ sQ7_spl
| ~ sQ20_spl
| big_p(sk7)
| ~ big_r(sk2(sk7),X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f270,f194]) ).
fof(f399,plain,
( ~ sQ7_spl
| ~ sQ20_spl
| sQ14_spl
| sQ25_spl ),
inference(split_clause,[status(thm)],[f397,f301,f239,f269,f193]) ).
fof(f412,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ27_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0)
| ~ big_p(sk5(sk7)) ),
inference(resolution,[status(thm)],[f309,f165]) ).
fof(f415,definition,
( sQ44_spl
<=> big_p(sk5(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition]) ).
fof(f417,plain,
( sQ44_spl
| ~ big_p(sk5(sk7)) ),
inference(component_clause,[status(thm)],[f415]) ).
fof(f418,plain,
( ~ sQ1_spl
| ~ sQ27_spl
| sQ26_spl
| ~ sQ44_spl ),
inference(split_clause,[status(thm)],[f412,f415,f304,f308,f164]) ).
fof(f436,plain,
! [X0] :
( ~ sQ5_spl
| sQ44_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f417,f183]) ).
fof(f449,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ25_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0)
| ~ big_p(sk1(sk7)) ),
inference(resolution,[status(thm)],[f302,f162]) ).
fof(f450,plain,
( ~ sQ6_spl
| ~ sQ25_spl
| big_p(sk7)
| ~ big_p(sk1(sk7)) ),
inference(resolution,[status(thm)],[f302,f189]) ).
fof(f453,definition,
( sQ48_spl
<=> big_p(sk1(sk7)) ),
introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition]) ).
fof(f455,plain,
( sQ48_spl
| ~ big_p(sk1(sk7)) ),
inference(component_clause,[status(thm)],[f453]) ).
fof(f456,plain,
( ~ sQ0_spl
| ~ sQ25_spl
| sQ26_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f449,f453,f304,f301,f161]) ).
fof(f457,plain,
( ~ sQ6_spl
| ~ sQ25_spl
| sQ14_spl
| ~ sQ48_spl ),
inference(split_clause,[status(thm)],[f450,f453,f239,f301,f188]) ).
fof(f463,plain,
! [X0] :
( ~ sQ4_spl
| sQ48_spl
| ~ big_r(sk7,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f455,f178]) ).
fof(f464,plain,
( ~ sQ11_spl
| sQ48_spl
| big_p(sk7) ),
inference(resolution,[status(thm)],[f455,f225]) ).
fof(f465,plain,
( ~ sQ4_spl
| sQ48_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f463,f304,f453,f177]) ).
fof(f466,plain,
( ~ sQ11_spl
| sQ48_spl
| sQ14_spl ),
inference(split_clause,[status(thm)],[f464,f239,f453,f224]) ).
fof(f467,plain,
( ~ sQ5_spl
| sQ44_spl
| sQ26_spl ),
inference(split_clause,[status(thm)],[f436,f304,f415,f182]) ).
fof(f487,plain,
! [X0] :
( ~ sQ0_spl
| ~ sQ33_spl
| ~ big_r(sk10,X0)
| ~ big_p(X0)
| ~ big_p(sk1(sk10)) ),
inference(resolution,[status(thm)],[f346,f162]) ).
fof(f489,definition,
( sQ53_spl
<=> big_p(sk1(sk10)) ),
introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition]) ).
fof(f491,plain,
( sQ53_spl
| ~ big_p(sk1(sk10)) ),
inference(component_clause,[status(thm)],[f489]) ).
fof(f493,plain,
( ~ sQ0_spl
| ~ sQ33_spl
| sQ34_spl
| ~ sQ53_spl ),
inference(split_clause,[status(thm)],[f487,f489,f348,f345,f161]) ).
fof(f502,plain,
! [X0] :
( ~ sQ4_spl
| sQ53_spl
| ~ big_r(sk10,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f491,f178]) ).
fof(f503,plain,
( ~ sQ4_spl
| sQ53_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f502,f348,f489,f177]) ).
fof(f534,plain,
( ~ sQ6_spl
| ~ sQ39_spl
| big_p(sk9)
| ~ big_p(sk1(sk9)) ),
inference(resolution,[status(thm)],[f375,f189]) ).
fof(f538,definition,
( sQ60_spl
<=> big_p(sk1(sk9)) ),
introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition]) ).
fof(f540,plain,
( sQ60_spl
| ~ big_p(sk1(sk9)) ),
inference(component_clause,[status(thm)],[f538]) ).
fof(f541,plain,
( ~ sQ6_spl
| ~ sQ39_spl
| sQ15_spl
| ~ sQ60_spl ),
inference(split_clause,[status(thm)],[f534,f538,f242,f374,f188]) ).
fof(f551,plain,
! [X0] :
( ~ sQ1_spl
| ~ sQ35_spl
| ~ big_r(sk10,X0)
| ~ big_p(X0)
| ~ big_p(sk5(sk10)) ),
inference(resolution,[status(thm)],[f353,f165]) ).
fof(f554,definition,
( sQ63_spl
<=> big_p(sk5(sk10)) ),
introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition]) ).
fof(f556,plain,
( sQ63_spl
| ~ big_p(sk5(sk10)) ),
inference(component_clause,[status(thm)],[f554]) ).
fof(f557,plain,
( ~ sQ1_spl
| ~ sQ35_spl
| sQ34_spl
| ~ sQ63_spl ),
inference(split_clause,[status(thm)],[f551,f554,f348,f352,f164]) ).
fof(f584,plain,
! [X0] :
( ~ sQ5_spl
| sQ63_spl
| ~ big_r(sk10,X0)
| ~ big_p(X0) ),
inference(resolution,[status(thm)],[f556,f183]) ).
fof(f585,plain,
( ~ sQ5_spl
| sQ63_spl
| sQ34_spl ),
inference(split_clause,[status(thm)],[f584,f348,f554,f182]) ).
fof(f591,plain,
( sQ60_spl
| ~ sQ11_spl
| big_p(sk9) ),
inference(resolution,[status(thm)],[f225,f540]) ).
fof(f592,plain,
( sQ60_spl
| ~ sQ11_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f591,f242,f224,f538]) ).
fof(f593,plain,
$false,
inference(sat_refutation,[status(thm)],[f167,f171,f175,f176,f180,f181,f185,f186,f187,f191,f196,f203,f204,f208,f210,f211,f215,f216,f217,f218,f219,f220,f221,f222,f223,f227,f230,f231,f232,f245,f249,f253,f257,f258,f259,f263,f264,f265,f266,f267,f268,f272,f273,f274,f275,f276,f277,f282,f288,f307,f311,f315,f316,f321,f329,f351,f355,f358,f369,f379,f399,f418,f456,f457,f465,f466,f467,f493,f503,f541,f557,f585,f592]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN067-2 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n020.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Mon Sep 21 10:42:49 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.59 % Drodi V4.1.1
% 0.09/0.61 % Refutation found
% 0.09/0.61 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.09/0.61 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.14/0.63 % Elapsed time: 0.041781 seconds
% 0.14/0.63 % CPU time: 0.137686 seconds
% 0.14/0.63 % Total memory used: 14.059 MB
% 0.14/0.63 % Net memory used: 13.960 MB
%------------------------------------------------------------------------------