%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV241-2 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:44:29 EDT 2024
% Result : Unsatisfiable 79.49s 79.65s
% Output : Refutation 79.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 11
% Syntax : Number of clauses : 26 ( 10 unt; 7 nHn; 21 RR)
% Number of literals : 53 ( 20 equ; 19 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 4 con; 0-3 aty)
% Number of variables : 43 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_2,negated_conjecture,
~ c_in(v_Y,c_Message_Oanalz(v_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(cls_conjecture_0,negated_conjecture,
c_in(v_Y,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(cls_Message_Oanalz__trans_0,axiom,
( ~ c_in(X18,c_Message_Oanalz(X19),tc_Message_Omsg)
| ~ c_lessequals(X19,c_Message_Oanalz(X17),tc_set(tc_Message_Omsg))
| c_in(X18,c_Message_Oanalz(X17),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oanalz__trans_0) ).
cnf(cls_Set_OsubsetI_1,axiom,
( ~ c_in(c_Main_OsubsetI__1(X32,X31,X30),X31,X30)
| c_lessequals(X32,X31,tc_set(X30)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_1) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_conjecture_1,negated_conjecture,
c_in(v_X,c_Message_Oanalz(v_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(c4,axiom,
( X58 != X56
| X59 != X57
| X60 != X61
| ~ c_in(X58,X59,X60)
| c_in(X56,X57,X61) ),
theory(equality) ).
cnf(c38,plain,
( v_X != X191
| c_Message_Oanalz(v_H) != X193
| tc_Message_Omsg != X192
| c_in(X191,X193,X192) ),
inference(resolution,[status(thm)],[c4,cls_conjecture_1]) ).
cnf(c154,plain,
( v_X != X195
| tc_Message_Omsg != X194
| c_in(X195,c_Message_Oanalz(v_H),X194) ),
inference(resolution,[status(thm)],[c38,reflexivity]) ).
cnf(c155,plain,
( v_X != X196
| c_in(X196,c_Message_Oanalz(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c154,reflexivity]) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(cls_Message_Oanalz_OInj_0,axiom,
( ~ c_in(X7,X6,tc_Message_Omsg)
| c_in(X7,c_Message_Oanalz(X6),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Oanalz_OInj_0) ).
cnf(cls_Set_OsubsetI_0,axiom,
( c_in(c_Main_OsubsetI__1(X25,X24,X23),X25,X23)
| c_lessequals(X25,X24,tc_set(X23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
cnf(cls_Set_OinsertE_0,axiom,
( ~ c_in(X29,c_insert(X27,X28,X26),X26)
| c_in(X29,X28,X26)
| X29 = X27 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OinsertE_0) ).
cnf(c16,plain,
( c_in(c_Main_OsubsetI__1(c_insert(X126,X125,X124),X123,X124),X125,X124)
| c_Main_OsubsetI__1(c_insert(X126,X125,X124),X123,X124) = X126
| c_lessequals(c_insert(X126,X125,X124),X123,tc_set(X124)) ),
inference(resolution,[status(thm)],[cls_Set_OinsertE_0,cls_Set_OsubsetI_0]) ).
cnf(c84,plain,
( c_Main_OsubsetI__1(c_insert(X438,X436,tc_Message_Omsg),X437,tc_Message_Omsg) = X438
| c_lessequals(c_insert(X438,X436,tc_Message_Omsg),X437,tc_set(tc_Message_Omsg))
| c_in(c_Main_OsubsetI__1(c_insert(X438,X436,tc_Message_Omsg),X437,tc_Message_Omsg),c_Message_Oanalz(X436),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c16,cls_Message_Oanalz_OInj_0]) ).
cnf(c819,plain,
( c_Main_OsubsetI__1(c_insert(X1112,X1113,tc_Message_Omsg),c_Message_Oanalz(X1113),tc_Message_Omsg) = X1112
| c_lessequals(c_insert(X1112,X1113,tc_Message_Omsg),c_Message_Oanalz(X1113),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[c84,cls_Set_OsubsetI_1]) ).
cnf(c4378,plain,
( c_Main_OsubsetI__1(c_insert(X7254,X7253,tc_Message_Omsg),c_Message_Oanalz(X7253),tc_Message_Omsg) = X7254
| ~ c_in(X7255,c_Message_Oanalz(c_insert(X7254,X7253,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(X7255,c_Message_Oanalz(X7253),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c819,cls_Message_Oanalz__trans_0]) ).
cnf(c101670,plain,
( c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oanalz(v_H),tc_Message_Omsg) = v_X
| c_in(v_Y,c_Message_Oanalz(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c4378,cls_conjecture_0]) ).
cnf(c102186,plain,
c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oanalz(v_H),tc_Message_Omsg) = v_X,
inference(resolution,[status(thm)],[c101670,cls_conjecture_2]) ).
cnf(c102208,plain,
v_X = c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oanalz(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c102186,symmetry]) ).
cnf(c102559,plain,
c_in(c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oanalz(v_H),tc_Message_Omsg),c_Message_Oanalz(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c102208,c155]) ).
cnf(c104076,plain,
c_lessequals(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Oanalz(v_H),tc_set(tc_Message_Omsg)),
inference(resolution,[status(thm)],[c102559,cls_Set_OsubsetI_1]) ).
cnf(c104099,plain,
( ~ c_in(X7295,c_Message_Oanalz(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(X7295,c_Message_Oanalz(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c104076,cls_Message_Oanalz__trans_0]) ).
cnf(c104499,plain,
c_in(v_Y,c_Message_Oanalz(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c104099,cls_conjecture_0]) ).
cnf(c104841,plain,
$false,
inference(resolution,[status(thm)],[c104499,cls_conjecture_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.14 % Problem : SWV241-2 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n004.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 : Thu May 9 05:51:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 79.49/79.65 % Version: 1.5
% 79.49/79.65 % SZS status Unsatisfiable
% 79.49/79.65 % SZS output start CNFRefutation
% See solution above
% 79.49/79.65
% 79.49/79.65 % Initial clauses : 17
% 79.49/79.65 % Processed clauses : 1355
% 79.49/79.65 % Factors computed : 137
% 79.49/79.65 % Resolvents computed: 105000
% 79.49/79.65 % Tautologies deleted: 3
% 79.49/79.65 % Forward subsumed : 1888
% 79.49/79.65 % Backward subsumed : 41
% 79.49/79.65 % -------- CPU Time ---------
% 79.49/79.65 % User time : 78.936 s
% 79.49/79.65 % System time : 0.352 s
% 79.49/79.65 % Total time : 79.288 s
%------------------------------------------------------------------------------