%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : SWV281-2 : TPTP v8.1.2. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:36 EDT 2024
% Result : Unsatisfiable 9.60s 9.78s
% Output : Refutation 9.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 11
% Syntax : Number of clauses : 29 ( 12 unt; 3 nHn; 13 RR)
% Number of literals : 58 ( 42 equ; 27 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 : 11 ( 11 usr; 6 con; 0-3 aty)
% Number of variables : 69 ( 12 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(cls_List_Olist_Odistinct__1_0,axiom,
c_List_Olist_ONil != c_List_Olist_OCons(X8,X7,X6),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_List_Olist_Odistinct__1_0) ).
cnf(cls_Nat_Onat__add__right__cancel_0,axiom,
( c_plus(X22,X20,tc_nat) != c_plus(X21,X20,tc_nat)
| X22 = X21 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onat__add__right__cancel_0) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(cls_Nat_Ole__add2_0,axiom,
c_lessequals(X14,c_plus(X15,X14,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Ole__add2_0) ).
cnf(cls_Public_ONonce__supply__lemma_0,axiom,
( ~ c_in(c_Message_Omsg_ONonce(X32),c_Event_Oused(X31),tc_Message_Omsg)
| ~ c_lessequals(v_sko__urX(X31),X32,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Public_ONonce__supply__lemma_0) ).
cnf(cls_conjecture_0,negated_conjecture,
( X11 = X10
| c_in(c_Message_Omsg_ONonce(X10),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X11),c_Event_Oused(v_evs),tc_Message_Omsg) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
cnf(c28,plain,
( ~ c_lessequals(v_sko__urX(v_evs),X143,tc_nat)
| X143 = X144
| c_in(c_Message_Omsg_ONonce(X144),c_Event_Oused(v_evs_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[cls_Public_ONonce__supply__lemma_0,cls_conjecture_0]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(cls_Nat_Oop_A_L_Oadd__0_0,axiom,
c_plus(c_0,X9,tc_nat) = X9,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Oop_A_L_Oadd__0_0) ).
cnf(transitivity,axiom,
( X18 != X17
| X17 != X16
| X18 = X16 ),
theory(equality) ).
cnf(c14,plain,
( X46 != c_plus(c_0,X47,tc_nat)
| X46 = X47 ),
inference(resolution,[status(thm)],[transitivity,cls_Nat_Oop_A_L_Oadd__0_0]) ).
cnf(c3,axiom,
( X56 != X54
| X53 != X52
| X57 != X55
| c_plus(X56,X53,X57) = c_plus(X54,X52,X55) ),
theory(equality) ).
cnf(c64,plain,
( X298 != X299
| X297 != X300
| c_plus(X298,X297,X296) = c_plus(X299,X300,X296) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c1459,plain,
( X311 != X314
| c_plus(X311,X312,X313) = c_plus(X314,X312,X313) ),
inference(resolution,[status(thm)],[c64,reflexivity]) ).
cnf(c1615,plain,
c_plus(c_plus(c_0,X328,tc_nat),X329,X327) = c_plus(X328,X329,X327),
inference(resolution,[status(thm)],[c1459,cls_Nat_Oop_A_L_Oadd__0_0]) ).
cnf(c1717,plain,
c_plus(c_plus(c_0,c_0,tc_nat),X331,tc_nat) = X331,
inference(resolution,[status(thm)],[c1615,c14]) ).
cnf(c6,axiom,
( X78 != X76
| X75 != X74
| X79 != X77
| ~ c_lessequals(X78,X75,X79)
| c_lessequals(X76,X74,X77) ),
theory(equality) ).
cnf(c103,plain,
( X463 != X466
| c_plus(X465,X463,tc_nat) != X462
| tc_nat != X464
| c_lessequals(X466,X462,X464) ),
inference(resolution,[status(thm)],[c6,cls_Nat_Ole__add2_0]) ).
cnf(c3403,plain,
( X467 != X469
| tc_nat != X468
| c_lessequals(X469,X467,X468) ),
inference(resolution,[status(thm)],[c103,c1717]) ).
cnf(c3422,plain,
( X470 != X471
| c_lessequals(X471,X470,tc_nat) ),
inference(resolution,[status(thm)],[c3403,reflexivity]) ).
cnf(c3433,plain,
c_lessequals(X472,X472,tc_nat),
inference(resolution,[status(thm)],[c3422,reflexivity]) ).
cnf(c3496,plain,
( v_sko__urX(v_evs) = X510
| c_in(c_Message_Omsg_ONonce(X510),c_Event_Oused(v_evs_H),tc_Message_Omsg) ),
inference(resolution,[status(thm)],[c3433,c28]) ).
cnf(c3907,plain,
( v_sko__urX(v_evs) = X511
| ~ c_lessequals(v_sko__urX(v_evs_H),X511,tc_nat) ),
inference(resolution,[status(thm)],[c3496,cls_Public_ONonce__supply__lemma_0]) ).
cnf(c3909,plain,
v_sko__urX(v_evs) = c_plus(X528,v_sko__urX(v_evs_H),tc_nat),
inference(resolution,[status(thm)],[c3907,cls_Nat_Ole__add2_0]) ).
cnf(c4535,plain,
c_plus(X534,v_sko__urX(v_evs_H),tc_nat) = v_sko__urX(v_evs),
inference(resolution,[status(thm)],[c3909,symmetry]) ).
cnf(c4521,plain,
( X833 != v_sko__urX(v_evs)
| X833 = c_plus(X834,v_sko__urX(v_evs_H),tc_nat) ),
inference(resolution,[status(thm)],[c3909,transitivity]) ).
cnf(c11521,plain,
c_plus(X1354,v_sko__urX(v_evs_H),tc_nat) = c_plus(X1353,v_sko__urX(v_evs_H),tc_nat),
inference(resolution,[status(thm)],[c4521,c4535]) ).
cnf(c25602,plain,
X1355 = X1356,
inference(resolution,[status(thm)],[c11521,cls_Nat_Onat__add__right__cancel_0]) ).
cnf(c25666,plain,
$false,
inference(resolution,[status(thm)],[c25602,cls_List_Olist_Odistinct__1_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : SWV281-2 : TPTP v8.1.2. Released v3.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n009.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:40:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 9.60/9.78 % Version: 1.5
% 9.60/9.78 % SZS status Unsatisfiable
% 9.60/9.78 % SZS output start CNFRefutation
% See solution above
% 9.60/9.78
% 9.60/9.78 % Initial clauses : 16
% 9.60/9.78 % Processed clauses : 551
% 9.60/9.78 % Factors computed : 69
% 9.60/9.78 % Resolvents computed: 25591
% 9.60/9.78 % Tautologies deleted: 4
% 9.60/9.78 % Forward subsumed : 612
% 9.60/9.78 % Backward subsumed : 407
% 9.60/9.78 % -------- CPU Time ---------
% 9.60/9.78 % User time : 9.360 s
% 9.60/9.78 % System time : 0.075 s
% 9.60/9.78 % Total time : 9.435 s
%------------------------------------------------------------------------------