%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN161-1 : TPTP v8.1.2. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:47:31 EDT 2024
% Result : Unsatisfiable 1.34s 1.51s
% Output : Refutation 1.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 19
% Syntax : Number of clauses : 44 ( 22 unt; 0 nHn; 22 RR)
% Number of literals : 76 ( 0 equ; 33 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 68 ( 33 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ n5(c,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
cnf(rule_314,axiom,
( n5(X13,X13)
| ~ r4(X13) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_314) ).
cnf(rule_240,axiom,
( n3(X46)
| ~ p2(X47,X48,X46) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_240) ).
cnf(axiom_19,axiom,
m0(X6,d,X5),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
cnf(rule_006,axiom,
( m1(X37,X37,X37)
| ~ m0(X36,X36,X37) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_006) ).
cnf(c44,plain,
m1(X38,X38,X38),
inference(resolution,[status(thm)],[rule_006,axiom_19]) ).
cnf(rule_150,axiom,
( p2(X211,X211,X211)
| ~ m1(X212,X212,X211) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_150) ).
cnf(c247,plain,
p2(X213,X213,X213),
inference(resolution,[status(thm)],[rule_150,c44]) ).
cnf(c252,plain,
n3(X217),
inference(resolution,[status(thm)],[c247,rule_240]) ).
cnf(axiom_30,axiom,
n0(e,e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_30) ).
cnf(rule_255,axiom,
( q3(X652,X650)
| ~ q2(X651,X652,X650)
| ~ n0(X651,X652) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_255) ).
cnf(rule_186,axiom,
( q2(X136,X136,X135)
| ~ l1(X135,X136) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_186) ).
cnf(axiom_9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
cnf(axiom_14,axiom,
p0(b,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
cnf(rule_003,axiom,
( l1(X21,X18)
| ~ p0(X19,X21)
| ~ r0(X20)
| ~ m0(X18,X21,X19) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_003) ).
cnf(c19,plain,
( l1(d,X727)
| ~ p0(X725,d)
| ~ r0(X726) ),
inference(resolution,[status(thm)],[rule_003,axiom_19]) ).
cnf(c875,plain,
( l1(d,X728)
| ~ r0(X729) ),
inference(resolution,[status(thm)],[c19,axiom_14]) ).
cnf(c876,plain,
l1(d,X734),
inference(resolution,[status(thm)],[c875,axiom_9]) ).
cnf(c880,plain,
q2(X736,X736,d),
inference(resolution,[status(thm)],[c876,rule_186]) ).
cnf(c881,plain,
( q3(X737,d)
| ~ n0(X737,X737) ),
inference(resolution,[status(thm)],[c880,rule_255]) ).
cnf(c884,plain,
q3(e,d),
inference(resolution,[status(thm)],[c881,axiom_30]) ).
cnf(rule_256,axiom,
( q3(X659,X659)
| ~ p2(X660,X659,X659)
| ~ q3(X660,X659) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_256) ).
cnf(axiom_13,axiom,
r0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_13) ).
cnf(rule_145,axiom,
( p2(e,X559,X558)
| ~ r0(e)
| ~ p1(X559,X558,e) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_145) ).
cnf(rule_082,axiom,
( p1(X372,X373,X375)
| ~ m0(X375,X372,X374)
| ~ p1(X375,X372,X374) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_082) ).
cnf(axiom_12,axiom,
m0(a,X7,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
cnf(rule_085,axiom,
( p1(X103,X103,X103)
| ~ p0(X104,X103) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_085) ).
cnf(c129,plain,
p1(X105,X105,X105),
inference(resolution,[status(thm)],[rule_085,axiom_14]) ).
cnf(c400,plain,
( p1(X382,X383,X382)
| ~ m0(X382,X382,X382) ),
inference(resolution,[status(thm)],[rule_082,c129]) ).
cnf(c414,plain,
p1(a,X388,a),
inference(resolution,[status(thm)],[c400,axiom_12]) ).
cnf(c418,plain,
( p1(X787,X788,a)
| ~ m0(a,X787,a) ),
inference(resolution,[status(thm)],[c414,rule_082]) ).
cnf(c970,plain,
p1(X790,X789,a),
inference(resolution,[status(thm)],[c418,axiom_12]) ).
cnf(c973,plain,
( p1(X805,X807,X806)
| ~ m0(X806,X805,a) ),
inference(resolution,[status(thm)],[c970,rule_082]) ).
cnf(c990,plain,
p1(d,X808,X809),
inference(resolution,[status(thm)],[c973,axiom_19]) ).
cnf(c994,plain,
( p2(e,d,X824)
| ~ r0(e) ),
inference(resolution,[status(thm)],[c990,rule_145]) ).
cnf(c1024,plain,
p2(e,d,X825),
inference(resolution,[status(thm)],[c994,axiom_13]) ).
cnf(c1028,plain,
( q3(d,d)
| ~ q3(e,d) ),
inference(resolution,[status(thm)],[c1024,rule_256]) ).
cnf(c1137,plain,
q3(d,d),
inference(resolution,[status(thm)],[c1028,c884]) ).
cnf(rule_298,axiom,
( r4(X1001)
| ~ n3(X1001)
| ~ q3(X998,X999)
| ~ p0(X1000,X1001) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_298) ).
cnf(c1247,plain,
( r4(X1002)
| ~ n3(X1002)
| ~ q3(X1003,X1004) ),
inference(resolution,[status(thm)],[rule_298,axiom_14]) ).
cnf(c1250,plain,
( r4(X1005)
| ~ n3(X1005) ),
inference(resolution,[status(thm)],[c1247,c1137]) ).
cnf(c1257,plain,
r4(X1006),
inference(resolution,[status(thm)],[c1250,c252]) ).
cnf(c1259,plain,
n5(X1007,X1007),
inference(resolution,[status(thm)],[c1257,rule_314]) ).
cnf(c1260,plain,
$false,
inference(resolution,[status(thm)],[c1259,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : SYN161-1 : TPTP v8.1.2. Released v1.1.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n018.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Wed May 8 19:47:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.34/1.51 % Version: 1.5
% 1.34/1.51 % SZS status Unsatisfiable
% 1.34/1.51 % SZS output start CNFRefutation
% See solution above
% 1.34/1.51
% 1.34/1.51 % Initial clauses : 369
% 1.34/1.51 % Processed clauses : 775
% 1.34/1.51 % Factors computed : 8
% 1.34/1.51 % Resolvents computed: 1253
% 1.34/1.51 % Tautologies deleted: 14
% 1.34/1.51 % Forward subsumed : 471
% 1.34/1.51 % Backward subsumed : 301
% 1.34/1.51 % -------- CPU Time ---------
% 1.34/1.51 % User time : 1.127 s
% 1.34/1.51 % System time : 0.023 s
% 1.34/1.51 % Total time : 1.150 s
%------------------------------------------------------------------------------