%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV274-2 : TPTP v8.1.2. Released v3.2.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:44:35 EDT 2024
% Result : Unsatisfiable 86.73s 86.90s
% Output : Refutation 86.73s
% 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_Osynth(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_Osynth(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_Osynth__trans_0,axiom,
( ~ c_in(X17,c_Message_Osynth(X19),tc_Message_Omsg)
| ~ c_lessequals(X19,c_Message_Osynth(X18),tc_set(tc_Message_Omsg))
| c_in(X17,c_Message_Osynth(X18),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Osynth__trans_0) ).
cnf(cls_Set_OsubsetI_1,axiom,
( ~ c_in(c_Main_OsubsetI__1(X30,X31,X32),X31,X32)
| c_lessequals(X30,X31,tc_set(X32)) ),
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_Osynth(v_H),tc_Message_Omsg),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
cnf(c4,axiom,
( X57 != X59
| X58 != X56
| X60 != X61
| ~ c_in(X57,X58,X60)
| c_in(X59,X56,X61) ),
theory(equality) ).
cnf(c38,plain,
( v_X != X193
| c_Message_Osynth(v_H) != X192
| tc_Message_Omsg != X191
| c_in(X193,X192,X191) ),
inference(resolution,[status(thm)],[c4,cls_conjecture_1]) ).
cnf(c154,plain,
( v_X != X195
| tc_Message_Omsg != X194
| c_in(X195,c_Message_Osynth(v_H),X194) ),
inference(resolution,[status(thm)],[c38,reflexivity]) ).
cnf(c155,plain,
( v_X != X196
| c_in(X196,c_Message_Osynth(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c154,reflexivity]) ).
cnf(symmetry,axiom,
( X3 != X4
| X4 = X3 ),
theory(equality) ).
cnf(cls_Message_Osynth_OInj_0,axiom,
( ~ c_in(X6,X7,tc_Message_Omsg)
| c_in(X6,c_Message_Osynth(X7),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Message_Osynth_OInj_0) ).
cnf(cls_Set_OsubsetI_0,axiom,
( c_in(c_Main_OsubsetI__1(X23,X24,X25),X23,X25)
| c_lessequals(X23,X24,tc_set(X25)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OsubsetI_0) ).
cnf(cls_Set_OinsertE_0,axiom,
( ~ c_in(X29,c_insert(X28,X27,X26),X26)
| c_in(X29,X27,X26)
| X29 = X28 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Set_OinsertE_0) ).
cnf(c16,plain,
( c_in(c_Main_OsubsetI__1(c_insert(X123,X125,X124),X126,X124),X125,X124)
| c_Main_OsubsetI__1(c_insert(X123,X125,X124),X126,X124) = X123
| c_lessequals(c_insert(X123,X125,X124),X126,tc_set(X124)) ),
inference(resolution,[status(thm)],[cls_Set_OinsertE_0,cls_Set_OsubsetI_0]) ).
cnf(c83,plain,
( c_Main_OsubsetI__1(c_insert(X415,X416,tc_Message_Omsg),X414,tc_Message_Omsg) = X415
| c_lessequals(c_insert(X415,X416,tc_Message_Omsg),X414,tc_set(tc_Message_Omsg))
| c_in(c_Main_OsubsetI__1(c_insert(X415,X416,tc_Message_Omsg),X414,tc_Message_Omsg),c_Message_Osynth(X416),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c16,cls_Message_Osynth_OInj_0]) ).
cnf(c769,plain,
( c_Main_OsubsetI__1(c_insert(X1083,X1082,tc_Message_Omsg),c_Message_Osynth(X1082),tc_Message_Omsg) = X1083
| c_lessequals(c_insert(X1083,X1082,tc_Message_Omsg),c_Message_Osynth(X1082),tc_set(tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[c83,cls_Set_OsubsetI_1]) ).
cnf(c4210,plain,
( c_Main_OsubsetI__1(c_insert(X7305,X7303,tc_Message_Omsg),c_Message_Osynth(X7303),tc_Message_Omsg) = X7305
| ~ c_in(X7304,c_Message_Osynth(c_insert(X7305,X7303,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(X7304,c_Message_Osynth(X7303),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c769,cls_Message_Osynth__trans_0]) ).
cnf(c105421,plain,
( c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Osynth(v_H),tc_Message_Omsg) = v_X
| c_in(v_Y,c_Message_Osynth(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c4210,cls_conjecture_0]) ).
cnf(c105895,plain,
c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Osynth(v_H),tc_Message_Omsg) = v_X,
inference(resolution,[status(thm)],[c105421,cls_conjecture_2]) ).
cnf(c106027,plain,
v_X = c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Osynth(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c105895,symmetry]) ).
cnf(c106675,plain,
c_in(c_Main_OsubsetI__1(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Osynth(v_H),tc_Message_Omsg),c_Message_Osynth(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c106027,c155]) ).
cnf(c107861,plain,
c_lessequals(c_insert(v_X,v_H,tc_Message_Omsg),c_Message_Osynth(v_H),tc_set(tc_Message_Omsg)),
inference(resolution,[status(thm)],[c106675,cls_Set_OsubsetI_1]) ).
cnf(c107879,plain,
( ~ c_in(X7352,c_Message_Osynth(c_insert(v_X,v_H,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(X7352,c_Message_Osynth(v_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c107861,cls_Message_Osynth__trans_0]) ).
cnf(c108268,plain,
c_in(v_Y,c_Message_Osynth(v_H),tc_Message_Omsg),
inference(resolution,[status(thm)],[c107879,cls_conjecture_0]) ).
cnf(c108616,plain,
$false,
inference(resolution,[status(thm)],[c108268,cls_conjecture_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : SWV274-2 : TPTP v8.1.2. Released v3.2.0.
% 0.09/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 : Thu May 9 06:04:38 EDT 2024
% 0.14/0.36 % CPUTime :
% 86.73/86.90 % Version: 1.5
% 86.73/86.90 % SZS status Unsatisfiable
% 86.73/86.90 % SZS output start CNFRefutation
% See solution above
% 86.73/86.90
% 86.73/86.90 % Initial clauses : 17
% 86.73/86.90 % Processed clauses : 1368
% 86.73/86.90 % Factors computed : 136
% 86.73/86.90 % Resolvents computed: 108481
% 86.73/86.90 % Tautologies deleted: 3
% 86.73/86.90 % Forward subsumed : 1906
% 86.73/86.90 % Backward subsumed : 42
% 86.73/86.90 % -------- CPU Time ---------
% 86.73/86.90 % User time : 86.138 s
% 86.73/86.90 % System time : 0.390 s
% 86.73/86.90 % Total time : 86.528 s
%------------------------------------------------------------------------------