%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SET821-2 : TPTP v8.1.2. Released v3.2.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:40:08 EDT 2024
% Result : Unsatisfiable 2.38s 2.55s
% Output : Refutation 2.38s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of clauses : 42 ( 14 unt; 15 nHn; 21 RR)
% Number of literals : 90 ( 24 equ; 31 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 105 ( 22 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_Set_OComplD__dest_0,axiom,
( ~ c_in(X5,X7,X6)
| ~ c_in(X5,c_uminus(X7,tc_set(X6)),X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OComplD__dest_0) ).
cnf(cls_Set_OComplI_0,axiom,
( c_in(X17,X19,X18)
| c_in(X17,c_uminus(X19,tc_set(X18)),X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OComplI_0) ).
cnf(c8,plain,
( c_in(X107,c_uminus(c_uminus(X108,tc_set(X106)),tc_set(X106)),X106)
| ~ c_in(X107,X108,X106) ),
inference(resolution,[status(thm)],[cls_Set_OComplI_0,cls_Set_OComplD__dest_0]) ).
cnf(cls_Set_OinsertCI_0,axiom,
( ~ c_in(X34,X33,X32)
| c_in(X34,c_insert(X31,X33,X32),X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OinsertCI_0) ).
cnf(cls_Set_OinsertCI_1,axiom,
c_in(X11,c_insert(X11,X12,X13),X13),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OinsertCI_1) ).
cnf(c15,plain,
c_in(X36,c_insert(X37,c_insert(X36,X38,X39),X39),X39),
inference(resolution,[status(thm)],[cls_Set_OinsertCI_0,cls_Set_OinsertCI_1]) ).
cnf(c16,plain,
c_in(X41,c_insert(X43,c_insert(X40,c_insert(X41,X42,X44),X44),X44),X44),
inference(resolution,[status(thm)],[c15,cls_Set_OinsertCI_0]) ).
cnf(c17,plain,
c_in(X139,c_insert(X140,c_insert(X142,c_insert(X141,c_insert(X139,X137,X138),X138),X138),X138),X138),
inference(resolution,[status(thm)],[c16,cls_Set_OinsertCI_0]) ).
cnf(c81,plain,
c_in(X862,c_uminus(c_uminus(c_insert(X857,c_insert(X859,c_insert(X860,c_insert(X862,X861,X858),X858),X858),X858),tc_set(X858)),tc_set(X858)),X858),
inference(resolution,[status(thm)],[c17,c8]) ).
cnf(c1044,plain,
~ c_in(X1494,c_uminus(c_insert(X1497,c_insert(X1495,c_insert(X1492,c_insert(X1494,X1496,X1493),X1493),X1493),X1493),tc_set(X1493)),X1493),
inference(resolution,[status(thm)],[c81,cls_Set_OComplD__dest_0]) ).
cnf(c49,plain,
c_in(X109,c_uminus(c_uminus(c_insert(X109,X110,X111),tc_set(X111)),tc_set(X111)),X111),
inference(resolution,[status(thm)],[c8,cls_Set_OinsertCI_1]) ).
cnf(c60,plain,
~ c_in(X113,c_uminus(c_insert(X113,X114,X112),tc_set(X112)),X112),
inference(resolution,[status(thm)],[c49,cls_Set_OComplD__dest_0]) ).
cnf(clsarity_IntDef__Oint_31,axiom,
class_Orderings_Oorder(tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_IntDef__Oint_31) ).
cnf(cls_Orderings_Oorder__less__irrefl__iff1_0,axiom,
( ~ class_Orderings_Oorder(X4)
| ~ c_less(X3,X3,X4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__less__irrefl__iff1_0) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_conjecture_1,negated_conjecture,
c_less(v_b,v_c,tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(c4,axiom,
( X92 != X97
| X95 != X96
| X94 != X93
| ~ c_less(X92,X95,X94)
| c_less(X97,X96,X93) ),
theory(equality) ).
cnf(c48,plain,
( v_b != X199
| v_c != X200
| tc_IntDef_Oint != X198
| c_less(X199,X200,X198) ),
inference(resolution,[status(thm)],[c4,cls_conjecture_1]) ).
cnf(c143,plain,
( v_b != X202
| v_c != X201
| c_less(X202,X201,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c48,reflexivity]) ).
cnf(c145,plain,
( v_b != X205
| c_less(X205,v_c,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c143,reflexivity]) ).
cnf(cls_conjecture_2,negated_conjecture,
( c_in(v_c,X52,tc_IntDef_Oint)
| ~ c_in(v_b,X52,tc_IntDef_Oint)
| c_in(v_a,X52,tc_IntDef_Oint) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(c22,plain,
( c_in(v_c,c_insert(v_b,X176,tc_IntDef_Oint),tc_IntDef_Oint)
| c_in(v_a,c_insert(v_b,X176,tc_IntDef_Oint),tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[cls_conjecture_2,cls_Set_OinsertCI_1]) ).
cnf(symmetry,axiom,
( X8 != X9
| X9 = X8 ),
theory(equality) ).
cnf(cls_Set_OinsertE_0,axiom,
( ~ c_in(X47,c_insert(X45,X48,X46),X46)
| c_in(X47,X48,X46)
| X47 = X45 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OinsertE_0) ).
cnf(c21,plain,
( c_in(X157,X158,X156)
| X157 = X155
| c_in(X157,c_uminus(c_insert(X155,X158,X156),tc_set(X156)),X156) ),
inference(resolution,[status(thm)],[cls_Set_OinsertE_0,cls_Set_OComplI_0]) ).
cnf(c94,plain,
( c_in(X326,X323,X325)
| c_in(X326,c_uminus(c_insert(X324,X323,X325),tc_set(X325)),X325)
| X324 = X326 ),
inference(resolution,[status(thm)],[c21,symmetry]) ).
cnf(c384,plain,
( c_in(X336,X335,X334)
| X337 = X336
| ~ c_in(X336,c_insert(X337,X335,X334),X334) ),
inference(resolution,[status(thm)],[c94,cls_Set_OComplD__dest_0]) ).
cnf(c417,plain,
( c_in(v_c,X1477,tc_IntDef_Oint)
| v_b = v_c
| c_in(v_a,c_insert(v_b,X1477,tc_IntDef_Oint),tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c384,c22]) ).
cnf(cls_conjecture_0,negated_conjecture,
c_less(v_a,v_b,tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(c47,plain,
( v_a != X190
| v_b != X191
| tc_IntDef_Oint != X189
| c_less(X190,X191,X189) ),
inference(resolution,[status(thm)],[c4,cls_conjecture_0]) ).
cnf(c129,plain,
( v_a != X196
| v_b != X195
| c_less(X196,X195,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c47,reflexivity]) ).
cnf(c139,plain,
( v_a != X197
| c_less(X197,v_b,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c129,reflexivity]) ).
cnf(c142,plain,
( c_less(X1955,v_b,tc_IntDef_Oint)
| c_in(v_a,X1954,X1956)
| c_in(v_a,c_uminus(c_insert(X1955,X1954,X1956),tc_set(X1956)),X1956) ),
inference(resolution,[status(thm)],[c139,c21]) ).
cnf(c5312,plain,
( c_in(v_a,X1999,X2000)
| c_in(v_a,c_uminus(c_insert(v_b,X1999,X2000),tc_set(X2000)),X2000)
| ~ class_Orderings_Oorder(tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c142,cls_Orderings_Oorder__less__irrefl__iff1_0]) ).
cnf(c5462,plain,
( c_in(v_a,X2002,X2001)
| c_in(v_a,c_uminus(c_insert(v_b,X2002,X2001),tc_set(X2001)),X2001) ),
inference(resolution,[status(thm)],[c5312,clsarity_IntDef__Oint_31]) ).
cnf(c5498,plain,
( c_in(v_a,X2012,X2011)
| ~ c_in(v_a,c_insert(v_b,X2012,X2011),X2011) ),
inference(resolution,[status(thm)],[c5462,cls_Set_OComplD__dest_0]) ).
cnf(c5601,plain,
( c_in(v_a,X2042,tc_IntDef_Oint)
| c_in(v_c,X2042,tc_IntDef_Oint)
| v_b = v_c ),
inference(resolution,[status(thm)],[c5498,c417]) ).
cnf(c5853,plain,
( c_in(v_a,X2070,tc_IntDef_Oint)
| c_in(v_c,X2070,tc_IntDef_Oint)
| c_less(v_c,v_c,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c5601,c145]) ).
cnf(c6061,plain,
( c_in(v_a,X2071,tc_IntDef_Oint)
| c_in(v_c,X2071,tc_IntDef_Oint)
| ~ class_Orderings_Oorder(tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c5853,cls_Orderings_Oorder__less__irrefl__iff1_0]) ).
cnf(c6064,plain,
( c_in(v_a,X2074,tc_IntDef_Oint)
| c_in(v_c,X2074,tc_IntDef_Oint) ),
inference(resolution,[status(thm)],[c6061,clsarity_IntDef__Oint_31]) ).
cnf(c6113,plain,
c_in(v_c,c_uminus(c_insert(v_a,X2075,tc_IntDef_Oint),tc_set(tc_IntDef_Oint)),tc_IntDef_Oint),
inference(resolution,[status(thm)],[c6064,c60]) ).
cnf(c6167,plain,
$false,
inference(resolution,[status(thm)],[c6113,c1044]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SET821-2 : TPTP v8.1.2. Released v3.2.0.
% 0.04/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n014.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed May 8 19:24:23 EDT 2024
% 0.14/0.36 % CPUTime :
% 2.38/2.55 % Version: 1.5
% 2.38/2.55 % SZS status Unsatisfiable
% 2.38/2.55 % SZS output start CNFRefutation
% See solution above
% 2.38/2.55
% 2.38/2.55 % Initial clauses : 19
% 2.38/2.55 % Processed clauses : 206
% 2.38/2.55 % Factors computed : 27
% 2.38/2.55 % Resolvents computed: 6147
% 2.38/2.55 % Tautologies deleted: 4
% 2.38/2.55 % Forward subsumed : 332
% 2.38/2.55 % Backward subsumed : 32
% 2.38/2.55 % -------- CPU Time ---------
% 2.38/2.55 % User time : 2.162 s
% 2.38/2.55 % System time : 0.026 s
% 2.38/2.55 % Total time : 2.188 s
%------------------------------------------------------------------------------