%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SYN353-1 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:48:00 EDT 2024
% Result : Unsatisfiable 6.95s 7.15s
% Output : Refutation 7.00s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 12
% Syntax : Number of clauses : 58 ( 10 unt; 34 nHn; 30 RR)
% Number of literals : 137 ( 0 equ; 41 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 1 con; 0-3 aty)
% Number of variables : 125 ( 9 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(clause2,negated_conjecture,
( ~ f(X25,X24,X23)
| f(X24,X23,X25)
| ~ f(X23,X24,z(X24,X23,X25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause2) ).
cnf(clause4,negated_conjecture,
( f(X4,X3,X2)
| f(X2,X3,z(X3,X2,X4)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause4) ).
cnf(clause8,negated_conjecture,
( f(X5,X6,X7)
| f(X7,z(X7,X5,X6),X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause8) ).
cnf(clause12,negated_conjecture,
( ~ f(X76,X75,X74)
| ~ f(X74,X76,X75)
| f(z(X75,X74,X76),X74,X75) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause12) ).
cnf(c103,plain,
( ~ f(X195,X196,X194)
| f(z(X196,X194,X195),X194,X196)
| f(X196,z(X196,X194,X195),X194) ),
inference(resolution,[status(thm)],[clause12,clause8]) ).
cnf(c657,plain,
( f(z(X521,X523,X522),X523,X521)
| f(X521,z(X521,X523,X522),X523)
| f(X523,X521,z(X521,X523,X522)) ),
inference(resolution,[status(thm)],[c103,clause4]) ).
cnf(clause1,negated_conjecture,
( ~ f(X18,X17,X19)
| ~ f(a,a,z(X18,X17,X19))
| f(X17,X19,X18)
| f(X19,X18,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause1) ).
cnf(clause6,negated_conjecture,
( ~ f(X43,X44,X45)
| f(X45,X43,X44)
| ~ f(X45,z(X45,X43,X44),X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause6) ).
cnf(clause10,negated_conjecture,
( f(X66,X65,X64)
| f(X65,X64,X66)
| ~ f(z(X65,X64,X66),X64,X65) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause10) ).
cnf(c9,plain,
( ~ f(a,a,X109)
| f(a,X109,a)
| f(X109,a,a) ),
inference(resolution,[status(thm)],[clause1,clause4]) ).
cnf(c4577,plain,
( f(z(a,a,X524),a,a)
| f(a,z(a,a,X524),a) ),
inference(resolution,[status(thm)],[c657,c9]) ).
cnf(c4599,plain,
( f(a,z(a,a,X693),a)
| f(X693,a,a)
| f(a,a,X693) ),
inference(resolution,[status(thm)],[c4577,clause10]) ).
cnf(c8189,plain,
( f(X694,a,a)
| f(a,a,X694)
| ~ f(a,X694,a) ),
inference(resolution,[status(thm)],[c4599,clause6]) ).
cnf(c8335,plain,
( f(z(a,a,X703),a,a)
| f(a,a,z(a,a,X703)) ),
inference(resolution,[status(thm)],[c8189,c657]) ).
cnf(clause11,negated_conjecture,
( f(X70,X71,X72)
| f(X72,X70,X71)
| ~ f(z(X72,X70,X71),X70,X72) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause11) ).
cnf(c8711,plain,
( f(a,a,z(a,a,X872))
| f(a,X872,a)
| f(a,a,X872) ),
inference(resolution,[status(thm)],[c8335,clause11]) ).
cnf(c12158,plain,
( f(a,X873,a)
| f(a,a,X873)
| ~ f(X873,a,a) ),
inference(resolution,[status(thm)],[c8711,clause2]) ).
cnf(c12315,plain,
( f(a,z(a,a,X881),a)
| f(a,a,z(a,a,X881)) ),
inference(resolution,[status(thm)],[c12158,c8335]) ).
cnf(clause3,negated_conjecture,
( ~ f(X31,X30,X29)
| f(X29,X31,X30)
| ~ f(X29,X30,z(X30,X29,X31)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause3) ).
cnf(c8340,plain,
( f(X704,a,a)
| f(a,a,X704)
| f(a,X704,z(X704,a,a)) ),
inference(resolution,[status(thm)],[c8189,clause4]) ).
cnf(clause7,negated_conjecture,
( ~ f(X50,X51,X52)
| f(X51,X52,X50)
| ~ f(X52,z(X52,X50,X51),X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause7) ).
cnf(c54,plain,
( ~ f(X163,X164,X162)
| f(X164,X162,X163)
| f(X163,z(X163,X162,z(X162,X163,X164)),X162) ),
inference(resolution,[status(thm)],[clause7,clause8]) ).
cnf(c375,plain,
( f(X453,X455,X454)
| f(X454,z(X454,X455,z(X455,X454,X453)),X455)
| f(X455,X453,z(X453,X455,X454)) ),
inference(resolution,[status(thm)],[c54,clause4]) ).
cnf(clause5,negated_conjecture,
( ~ f(X36,X35,X37)
| ~ f(X35,X37,X36)
| f(X35,X36,z(X36,X35,X37)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause5) ).
cnf(c49,plain,
( ~ f(X161,X160,X159)
| f(X159,X161,X160)
| f(X161,z(X161,X159,z(X159,X161,X160)),X159) ),
inference(resolution,[status(thm)],[clause6,clause8]) ).
cnf(c343,plain,
( f(X443,X442,X441)
| f(X442,z(X442,X443,z(X443,X442,X441)),X443)
| f(X443,X441,z(X441,X443,X442)) ),
inference(resolution,[status(thm)],[c49,clause4]) ).
cnf(c3391,plain,
( f(X621,z(X621,X619,z(X619,X621,X620)),X619)
| f(X619,X620,z(X620,X619,X621))
| ~ f(X620,X619,X621) ),
inference(resolution,[status(thm)],[c343,clause5]) ).
cnf(c6425,plain,
( f(X624,z(X624,X623,z(X623,X624,X622)),X623)
| f(X623,X622,z(X622,X623,X624)) ),
inference(resolution,[status(thm)],[c3391,c375]) ).
cnf(c6433,plain,
( f(X787,X785,z(X785,X787,X786))
| ~ f(X787,z(X787,X786,X785),X786)
| f(X786,X787,z(X787,X786,X785)) ),
inference(resolution,[status(thm)],[c6425,clause6]) ).
cnf(c12760,plain,
( f(a,a,z(a,a,X882))
| f(a,X882,z(X882,a,a)) ),
inference(resolution,[status(thm)],[c12315,c6433]) ).
cnf(c12877,plain,
( f(a,X905,z(X905,a,a))
| ~ f(X905,a,a)
| f(a,a,X905) ),
inference(resolution,[status(thm)],[c12760,clause2]) ).
cnf(c13862,plain,
( f(a,X906,z(X906,a,a))
| f(a,a,X906) ),
inference(resolution,[status(thm)],[c12877,c8340]) ).
cnf(c13972,plain,
( f(a,a,X907)
| ~ f(a,X907,a) ),
inference(resolution,[status(thm)],[c13862,clause3]) ).
cnf(c14053,plain,
f(a,a,z(a,a,X908)),
inference(resolution,[status(thm)],[c13972,c12315]) ).
cnf(c14143,plain,
( ~ f(X912,a,a)
| f(a,a,X912) ),
inference(resolution,[status(thm)],[c14053,clause2]) ).
cnf(c14168,plain,
( ~ f(X913,a,a)
| f(a,X913,a) ),
inference(resolution,[status(thm)],[c14053,clause3]) ).
cnf(c14341,plain,
f(a,z(a,a,X914),a),
inference(resolution,[status(thm)],[c14168,c4577]) ).
cnf(c14364,plain,
( ~ f(a,X919,a)
| f(X919,a,a) ),
inference(resolution,[status(thm)],[c14341,clause7]) ).
cnf(c14428,plain,
f(z(a,a,X920),a,a),
inference(resolution,[status(thm)],[c14364,c14341]) ).
cnf(c14497,plain,
( f(X927,a,a)
| f(a,a,X927) ),
inference(resolution,[status(thm)],[c14428,clause10]) ).
cnf(c14726,plain,
f(a,a,X928),
inference(resolution,[status(thm)],[c14497,c14143]) ).
cnf(c14797,plain,
( ~ f(X959,X960,X961)
| f(X960,X961,X959)
| f(X961,X959,X960) ),
inference(resolution,[status(thm)],[c14726,clause1]) ).
cnf(c15277,plain,
( f(X973,X974,z(X974,X973,X972))
| f(X974,z(X974,X973,X972),X973) ),
inference(resolution,[status(thm)],[c14797,c657]) ).
cnf(c15241,plain,
( f(X1084,X1085,X1083)
| f(X1085,X1083,X1084)
| f(X1085,z(X1085,X1083,X1084),X1083) ),
inference(resolution,[status(thm)],[c14797,clause8]) ).
cnf(c15536,plain,
( f(X1128,z(X1128,X1127,X1126),X1127)
| ~ f(X1126,X1128,X1127)
| f(X1128,X1127,X1126) ),
inference(resolution,[status(thm)],[c15277,clause2]) ).
cnf(c19101,plain,
( f(X1131,z(X1131,X1130,X1129),X1130)
| f(X1131,X1130,X1129) ),
inference(resolution,[status(thm)],[c15536,c15241]) ).
cnf(c19164,plain,
( f(X1132,X1134,X1133)
| ~ f(X1134,X1133,X1132) ),
inference(resolution,[status(thm)],[c19101,clause6]) ).
cnf(c19260,plain,
f(X1142,X1141,z(X1141,X1142,X1143)),
inference(resolution,[status(thm)],[c19164,c15277]) ).
cnf(c19497,plain,
( ~ f(X1166,X1165,X1164)
| f(X1165,X1164,X1166) ),
inference(resolution,[status(thm)],[c19260,clause2]) ).
cnf(c15224,plain,
( f(z(X971,X970,X969),X970,X971)
| f(X970,X971,z(X971,X970,X969)) ),
inference(resolution,[status(thm)],[c14797,c657]) ).
cnf(c19349,plain,
f(z(X1147,X1149,X1148),X1149,X1147),
inference(resolution,[status(thm)],[c19164,c15224]) ).
cnf(c19540,plain,
( f(X1190,X1189,X1188)
| f(X1189,X1188,X1190) ),
inference(resolution,[status(thm)],[c19349,clause10]) ).
cnf(c19579,plain,
f(X1192,X1193,X1194),
inference(resolution,[status(thm)],[c19540,c19497]) ).
cnf(clause17,negated_conjecture,
( ~ f(X123,X122,X124)
| ~ f(X122,X124,X123)
| ~ f(X124,X123,X122)
| ~ f(z(X123,X122,X124),z(X123,X122,X124),z(X123,X122,X124)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clause17) ).
cnf(c19577,plain,
f(X1191,X1191,X1191),
inference(factor,[status(thm)],[c19540]) ).
cnf(c19586,plain,
( ~ f(X1259,X1260,X1261)
| ~ f(X1260,X1261,X1259)
| ~ f(X1261,X1259,X1260) ),
inference(resolution,[status(thm)],[c19577,clause17]) ).
cnf(c19588,plain,
~ f(X1262,X1262,X1262),
inference(factor,[status(thm)],[c19586]) ).
cnf(c19591,plain,
$false,
inference(resolution,[status(thm)],[c19588,c19579]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : SYN353-1 : TPTP v8.1.2. Released v1.2.0.
% 0.14/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.37 % Computer : n021.cluster.edu
% 0.14/0.37 % Model : x86_64 x86_64
% 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.37 % Memory : 8042.1875MB
% 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Wed May 8 20:20:08 EDT 2024
% 0.14/0.37 % CPUTime :
% 6.95/7.15 % Version: 1.5
% 6.95/7.15 % SZS status Unsatisfiable
% 6.95/7.15 % SZS output start CNFRefutation
% See solution above
% 7.00/7.15
% 7.00/7.15 % Initial clauses : 17
% 7.00/7.15 % Processed clauses : 254
% 7.00/7.15 % Factors computed : 47
% 7.00/7.15 % Resolvents computed: 19545
% 7.00/7.15 % Tautologies deleted: 19
% 7.00/7.15 % Forward subsumed : 393
% 7.00/7.15 % Backward subsumed : 251
% 7.00/7.15 % -------- CPU Time ---------
% 7.00/7.15 % User time : 6.722 s
% 7.00/7.15 % System time : 0.055 s
% 7.00/7.15 % Total time : 6.777 s
%------------------------------------------------------------------------------