%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT033-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:29:09 EDT 2024
% Result : Unsatisfiable 1.21s 1.38s
% Output : Refutation 1.21s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of clauses : 25 ( 15 unt; 0 nHn; 10 RR)
% Number of literals : 38 ( 37 equ; 14 neg)
% Maximal clause size : 3 ( 1 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 1 con; 0-2 aty)
% Number of variables : 54 ( 10 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(idempotence_of_join,negated_conjecture,
join(xx,xx) != xx,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_of_join) ).
cnf(transitivity,axiom,
( X31 != X29
| X29 != X30
| X31 = X30 ),
theory(equality) ).
cnf(commutativity_of_join,axiom,
join(X13,X12) = join(X12,X13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_join) ).
cnf(absorption2,axiom,
join(X9,meet(X9,X8)) = X9,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption2) ).
cnf(c13,plain,
( X54 != join(X56,meet(X56,X55))
| X54 = X56 ),
inference(resolution,[status(thm)],[transitivity,absorption2]) ).
cnf(c47,plain,
join(meet(X59,X58),X59) = X59,
inference(resolution,[status(thm)],[c13,commutativity_of_join]) ).
cnf(c53,plain,
( X140 != join(meet(X142,X141),X142)
| X140 = X142 ),
inference(resolution,[status(thm)],[c47,transitivity]) ).
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c1,axiom,
( X60 != X63
| X61 != X62
| join(X60,X61) = join(X63,X62) ),
theory(equality) ).
cnf(c66,plain,
( X156 != X154
| join(X156,X155) = join(X154,X155) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(symmetry,axiom,
( X4 != X3
| X3 = X4 ),
theory(equality) ).
cnf(commutativity_of_meet,axiom,
meet(X11,X10) = meet(X10,X11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_meet) ).
cnf(absorption1,axiom,
meet(X7,join(X7,X6)) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',absorption1) ).
cnf(c12,plain,
( X38 != meet(X40,join(X40,X39))
| X38 = X40 ),
inference(resolution,[status(thm)],[transitivity,absorption1]) ).
cnf(c24,plain,
meet(join(X43,X42),X43) = X43,
inference(resolution,[status(thm)],[c12,commutativity_of_meet]) ).
cnf(c28,plain,
( X112 != meet(join(X113,X114),X113)
| X112 = X113 ),
inference(resolution,[status(thm)],[c24,transitivity]) ).
cnf(c4,plain,
X17 = join(X17,meet(X17,X16)),
inference(resolution,[status(thm)],[absorption2,symmetry]) ).
cnf(c0,axiom,
( X46 != X49
| X47 != X48
| meet(X46,X47) = meet(X49,X48) ),
theory(equality) ).
cnf(c39,plain,
( X127 != X128
| meet(X127,X129) = meet(X128,X129) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c180,plain,
meet(X532,X534) = meet(join(X532,meet(X532,X533)),X534),
inference(resolution,[status(thm)],[c39,c4]) ).
cnf(c2810,plain,
meet(X539,X539) = X539,
inference(resolution,[status(thm)],[c180,c28]) ).
cnf(c2900,plain,
X540 = meet(X540,X540),
inference(resolution,[status(thm)],[c2810,symmetry]) ).
cnf(c2943,plain,
join(X621,X622) = join(meet(X621,X621),X622),
inference(resolution,[status(thm)],[c2900,c66]) ).
cnf(c3977,plain,
join(X623,X623) = X623,
inference(resolution,[status(thm)],[c2943,c53]) ).
cnf(c4017,plain,
$false,
inference(resolution,[status(thm)],[c3977,idempotence_of_join]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.10 % Problem : LAT033-1 : TPTP v8.1.2. Bugfixed v2.5.0.
% 0.03/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.30 % WCLimit : 300
% 0.10/0.30 % DateTime : Wed May 8 12:37:37 EDT 2024
% 0.10/0.30 % CPUTime :
% 1.21/1.38 % Version: 1.5
% 1.21/1.38 % SZS status Unsatisfiable
% 1.21/1.38 % SZS output start CNFRefutation
% See solution above
% 1.21/1.38
% 1.21/1.38 % Initial clauses : 12
% 1.21/1.38 % Processed clauses : 144
% 1.21/1.38 % Factors computed : 3
% 1.21/1.38 % Resolvents computed: 4044
% 1.21/1.38 % Tautologies deleted: 2
% 1.21/1.38 % Forward subsumed : 128
% 1.21/1.38 % Backward subsumed : 0
% 1.21/1.38 % -------- CPU Time ---------
% 1.21/1.38 % User time : 1.060 s
% 1.21/1.38 % System time : 0.022 s
% 1.21/1.38 % Total time : 1.082 s
%------------------------------------------------------------------------------