%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV250-2 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:31 EDT 2024
% Result : Unsatisfiable 20.91s 21.09s
% Output : Refutation 20.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 12
% Syntax : Number of clauses : 29 ( 14 unt; 3 nHn; 15 RR)
% Number of literals : 55 ( 33 equ; 24 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-3 aty)
% Number of variables : 66 ( 4 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_conjecture_3,negated_conjecture,
~ c_in(v_x,c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_3) ).
cnf(cls_Set_OUn__iff_2,axiom,
( ~ c_in(X22,X24,X23)
| c_in(X22,c_union(X25,X24,X23),X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_2) ).
cnf(cls_Set_OUn__iff_1,axiom,
( ~ c_in(X18,X21,X20)
| c_in(X18,c_union(X21,X19,X20),X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_1) ).
cnf(cls_Set_OUn__iff_0,axiom,
( ~ c_in(X26,c_union(X29,X28,X27),X27)
| c_in(X26,X28,X27)
| c_in(X26,X29,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Set_OUn__iff_0) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_conjecture_2,negated_conjecture,
c_in(v_x,c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_2) ).
cnf(c3,axiom,
( X43 != X39
| X38 != X41
| X40 != X42
| ~ c_in(X43,X38,X40)
| c_in(X39,X41,X42) ),
theory(equality) ).
cnf(c23,plain,
( v_x != X179
| c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),v_H,tc_Message_Omsg)) != X178
| tc_Message_Omsg != X177
| c_in(X179,X178,X177) ),
inference(resolution,[status(thm)],[c3,cls_conjecture_2]) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(cls_Message_Oanalz__analz__Un_0,axiom,
c_Message_Oanalz(c_union(c_Message_Oanalz(X31),X30,tc_Message_Omsg)) = c_Message_Oanalz(c_union(X31,X30,tc_Message_Omsg)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Oanalz__analz__Un_0) ).
cnf(c14,plain,
c_Message_Oanalz(c_union(X33,X32,tc_Message_Omsg)) = c_Message_Oanalz(c_union(c_Message_Oanalz(X33),X32,tc_Message_Omsg)),
inference(resolution,[status(thm)],[cls_Message_Oanalz__analz__Un_0,symmetry]) ).
cnf(c1,axiom,
( X49 != X45
| X44 != X47
| X46 != X48
| c_union(X49,X44,X46) = c_union(X45,X47,X48) ),
theory(equality) ).
cnf(c26,plain,
( X78 != X79
| X75 != X77
| c_union(X78,X75,X76) = c_union(X79,X77,X76) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c61,plain,
( X89 != X87
| c_union(X89,X88,X90) = c_union(X87,X88,X90) ),
inference(resolution,[status(thm)],[c26,reflexivity]) ).
cnf(c82,plain,
c_union(c_Message_Oanalz(c_union(X271,X273,tc_Message_Omsg)),X272,X274) = c_union(c_Message_Oanalz(c_union(c_Message_Oanalz(X271),X273,tc_Message_Omsg)),X272,X274),
inference(resolution,[status(thm)],[c61,c14]) ).
cnf(transitivity,axiom,
( X8 != X6
| X6 != X7
| X8 = X7 ),
theory(equality) ).
cnf(cls_Message_Oanalz__synth__Un_0,axiom,
c_Message_Oanalz(c_union(c_Message_Osynth(X35),X34,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(X35,X34,tc_Message_Omsg)),c_Message_Osynth(X35),tc_Message_Omsg),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Message_Oanalz__synth__Un_0) ).
cnf(c22,plain,
c_union(c_Message_Oanalz(c_union(X164,X165,tc_Message_Omsg)),c_Message_Osynth(X164),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(X164),X165,tc_Message_Omsg)),
inference(resolution,[status(thm)],[cls_Message_Oanalz__synth__Un_0,symmetry]) ).
cnf(c240,plain,
( X857 != c_union(c_Message_Oanalz(c_union(X859,X858,tc_Message_Omsg)),c_Message_Osynth(X859),tc_Message_Omsg)
| X857 = c_Message_Oanalz(c_union(c_Message_Osynth(X859),X858,tc_Message_Omsg)) ),
inference(resolution,[status(thm)],[c22,transitivity]) ).
cnf(c3162,plain,
c_union(c_Message_Oanalz(c_union(X914,X913,tc_Message_Omsg)),c_Message_Osynth(c_Message_Oanalz(X914)),tc_Message_Omsg) = c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(X914)),X913,tc_Message_Omsg)),
inference(resolution,[status(thm)],[c240,c82]) ).
cnf(c3631,plain,
c_Message_Oanalz(c_union(c_Message_Osynth(c_Message_Oanalz(X929)),X928,tc_Message_Omsg)) = c_union(c_Message_Oanalz(c_union(X929,X928,tc_Message_Omsg)),c_Message_Osynth(c_Message_Oanalz(X929)),tc_Message_Omsg),
inference(resolution,[status(thm)],[c3162,symmetry]) ).
cnf(c3823,plain,
( v_x != X3572
| tc_Message_Omsg != X3573
| c_in(X3572,c_union(c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),X3573) ),
inference(resolution,[status(thm)],[c3631,c23]) ).
cnf(c43693,plain,
( v_x != X3574
| c_in(X3574,c_union(c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c3823,reflexivity]) ).
cnf(c43694,plain,
c_in(v_x,c_union(c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg),tc_Message_Omsg),
inference(resolution,[status(thm)],[c43693,reflexivity]) ).
cnf(c43982,plain,
( c_in(v_x,c_Message_Osynth(c_Message_Oanalz(v_G)),tc_Message_Omsg)
| c_in(v_x,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c43694,cls_Set_OUn__iff_0]) ).
cnf(c43988,plain,
( c_in(v_x,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg)
| c_in(v_x,c_union(c_Message_Osynth(c_Message_Oanalz(v_G)),X3590,tc_Message_Omsg),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c43982,cls_Set_OUn__iff_1]) ).
cnf(c44301,plain,
c_in(v_x,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),
inference(resolution,[status(thm)],[c43988,cls_conjecture_3]) ).
cnf(c44302,plain,
c_in(v_x,c_union(X3591,c_Message_Oanalz(c_union(v_G,v_H,tc_Message_Omsg)),tc_Message_Omsg),tc_Message_Omsg),
inference(resolution,[status(thm)],[c44301,cls_Set_OUn__iff_2]) ).
cnf(c44309,plain,
$false,
inference(resolution,[status(thm)],[c44302,cls_conjecture_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWV250-2 : TPTP v8.1.2. Released v3.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 05:08:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 20.91/21.09 % Version: 1.5
% 20.91/21.09 % SZS status Unsatisfiable
% 20.91/21.09 % SZS output start CNFRefutation
% See solution above
% 20.91/21.09
% 20.91/21.09 % Initial clauses : 14
% 20.91/21.09 % Processed clauses : 617
% 20.91/21.09 % Factors computed : 26
% 20.91/21.09 % Resolvents computed: 44280
% 20.91/21.09 % Tautologies deleted: 2
% 20.91/21.09 % Forward subsumed : 746
% 20.91/21.09 % Backward subsumed : 44
% 20.91/21.09 % -------- CPU Time ---------
% 20.91/21.09 % User time : 20.589 s
% 20.91/21.09 % System time : 0.146 s
% 20.91/21.09 % Total time : 20.735 s
%------------------------------------------------------------------------------