%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN180-1 : TPTP v8.1.2. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n014.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:33 EDT 2024
% Result : Unsatisfiable 1.93s 2.08s
% Output : Refutation 1.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 23
% Syntax : Number of clauses : 52 ( 25 unt; 0 nHn; 26 RR)
% Number of literals : 98 ( 0 equ; 47 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 20 ( 19 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 84 ( 40 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_this,negated_conjecture,
~ q4(a,e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this) ).
cnf(axiom_1,axiom,
s0(d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_1) ).
cnf(axiom_37,axiom,
n0(b,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_37) ).
cnf(rule_002,axiom,
( l1(X16,X16)
| ~ n0(X15,X16) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_002) ).
cnf(c13,plain,
l1(a,a),
inference(resolution,[status(thm)],[rule_002,axiom_37]) ).
cnf(rule_135,axiom,
( m2(X195)
| ~ s0(X195)
| ~ l1(X197,X196) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_135) ).
cnf(c228,plain,
( m2(X198)
| ~ s0(X198) ),
inference(resolution,[status(thm)],[rule_135,c13]) ).
cnf(c234,plain,
m2(d),
inference(resolution,[status(thm)],[c228,axiom_1]) ).
cnf(rule_201,axiom,
( k3(X706,X706,X705)
| ~ p1(X705,X704,X706)
| ~ m2(X707)
| ~ m2(X704) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_201) ).
cnf(axiom_12,axiom,
m0(a,X6,a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_12) ).
cnf(rule_082,axiom,
( p1(X371,X372,X374)
| ~ m0(X374,X371,X373)
| ~ p1(X374,X371,X373) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_082) ).
cnf(axiom_14,axiom,
p0(b,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_14) ).
cnf(rule_085,axiom,
( p1(X103,X103,X103)
| ~ p0(X102,X103) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_085) ).
cnf(c129,plain,
p1(X104,X104,X104),
inference(resolution,[status(thm)],[rule_085,axiom_14]) ).
cnf(c402,plain,
( p1(X382,X381,X382)
| ~ m0(X382,X382,X382) ),
inference(resolution,[status(thm)],[rule_082,c129]) ).
cnf(c414,plain,
p1(a,X387,a),
inference(resolution,[status(thm)],[c402,axiom_12]) ).
cnf(c417,plain,
( p1(X784,X785,a)
| ~ m0(a,X784,a) ),
inference(resolution,[status(thm)],[c414,rule_082]) ).
cnf(c955,plain,
p1(X786,X787,a),
inference(resolution,[status(thm)],[c417,axiom_12]) ).
cnf(c958,plain,
( k3(a,a,X1055)
| ~ m2(X1056)
| ~ m2(X1054) ),
inference(resolution,[status(thm)],[c955,rule_201]) ).
cnf(c1303,plain,
( k3(a,a,X1058)
| ~ m2(X1057) ),
inference(factor,[status(thm)],[c958]) ).
cnf(c1306,plain,
k3(a,a,X1059),
inference(resolution,[status(thm)],[c1303,c234]) ).
cnf(rule_236,axiom,
( m3(X41,X41,X41)
| ~ n2(X41) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_236) ).
cnf(rule_137,axiom,
( n2(X33)
| ~ p1(X34,X32,X33) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_137) ).
cnf(c130,plain,
n2(X108),
inference(resolution,[status(thm)],[c129,rule_137]) ).
cnf(c132,plain,
m3(X110,X110,X110),
inference(resolution,[status(thm)],[c130,rule_236]) ).
cnf(rule_295,axiom,
( q4(X988,X992)
| ~ k3(X989,X989,X988)
| ~ q2(X991,X992,X988)
| ~ m3(X991,X990,X991) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_295) ).
cnf(c1226,plain,
( q4(X1363,X1365)
| ~ k3(X1362,X1362,X1363)
| ~ q2(X1364,X1365,X1363) ),
inference(resolution,[status(thm)],[rule_295,c132]) ).
cnf(axiom_17,axiom,
q0(X3,d),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_17) ).
cnf(axiom_9,axiom,
r0(b),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_9) ).
cnf(axiom_20,axiom,
l0(a),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_20) ).
cnf(axiom_19,axiom,
m0(X4,d,X5),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_19) ).
cnf(rule_015,axiom,
( m1(X78,X77,X77)
| ~ l0(X76)
| ~ m0(X77,X77,X78) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_015) ).
cnf(c73,plain,
( m1(X268,d,d)
| ~ l0(X269) ),
inference(resolution,[status(thm)],[rule_015,axiom_19]) ).
cnf(c309,plain,
m1(X270,d,d),
inference(resolution,[status(thm)],[c73,axiom_20]) ).
cnf(rule_113,axiom,
( q1(X476,X476,X477)
| ~ r0(X478)
| ~ m1(X476,X477,X477) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_113) ).
cnf(c501,plain,
( q1(X481,X481,d)
| ~ r0(X482) ),
inference(resolution,[status(thm)],[rule_113,c309]) ).
cnf(c503,plain,
q1(X483,X483,d),
inference(resolution,[status(thm)],[c501,axiom_9]) ).
cnf(rule_124,axiom,
( r1(X514)
| ~ q0(X514,X515)
| ~ s0(d)
| ~ q1(d,X515,d) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_124) ).
cnf(c528,plain,
( r1(X527)
| ~ q0(X527,d)
| ~ s0(d) ),
inference(resolution,[status(thm)],[rule_124,c503]) ).
cnf(c546,plain,
( r1(X528)
| ~ s0(d) ),
inference(resolution,[status(thm)],[c528,axiom_17]) ).
cnf(c547,plain,
r1(X529),
inference(resolution,[status(thm)],[c546,axiom_1]) ).
cnf(axiom_28,axiom,
k0(e),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',axiom_28) ).
cnf(rule_181,axiom,
( q2(X229,X229,X229)
| ~ p1(X229,X229,X229) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_181) ).
cnf(c272,plain,
q2(X230,X230,X230),
inference(resolution,[status(thm)],[rule_181,c129]) ).
cnf(rule_187,axiom,
( q2(X681,X680,X681)
| ~ r1(X680)
| ~ m0(X683,X682,X681)
| ~ k0(X680)
| ~ q2(X680,X680,X680) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SYN001-0.ax',rule_187) ).
cnf(c770,plain,
( q2(X1491,X1492,X1491)
| ~ r1(X1492)
| ~ m0(X1490,X1493,X1491)
| ~ k0(X1492) ),
inference(resolution,[status(thm)],[rule_187,c272]) ).
cnf(c1976,plain,
( q2(X1494,X1495,X1494)
| ~ r1(X1495)
| ~ k0(X1495) ),
inference(resolution,[status(thm)],[c770,axiom_19]) ).
cnf(c1982,plain,
( q2(X1496,e,X1496)
| ~ r1(e) ),
inference(resolution,[status(thm)],[c1976,axiom_28]) ).
cnf(c1984,plain,
q2(X1497,e,X1497),
inference(resolution,[status(thm)],[c1982,c547]) ).
cnf(c1988,plain,
( q4(X1509,e)
| ~ k3(X1510,X1510,X1509) ),
inference(resolution,[status(thm)],[c1984,c1226]) ).
cnf(c2010,plain,
q4(X1511,e),
inference(resolution,[status(thm)],[c1988,c1306]) ).
cnf(c2022,plain,
$false,
inference(resolution,[status(thm)],[c2010,prove_this]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : SYN180-1 : TPTP v8.1.2. Released v1.1.0.
% 0.08/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n014.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 20:13:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 1.93/2.08 % Version: 1.5
% 1.93/2.08 % SZS status Unsatisfiable
% 1.93/2.08 % SZS output start CNFRefutation
% See solution above
% 1.93/2.08
% 1.93/2.08 % Initial clauses : 369
% 1.93/2.08 % Processed clauses : 1136
% 1.93/2.08 % Factors computed : 10
% 1.93/2.08 % Resolvents computed: 2013
% 1.93/2.08 % Tautologies deleted: 15
% 1.93/2.08 % Forward subsumed : 873
% 1.93/2.08 % Backward subsumed : 507
% 1.93/2.08 % -------- CPU Time ---------
% 1.93/2.08 % User time : 1.707 s
% 1.93/2.08 % System time : 0.012 s
% 1.93/2.08 % Total time : 1.719 s
%------------------------------------------------------------------------------