%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : LAT005-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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:06 EDT 2024
% Result : Unsatisfiable 110.06s 110.25s
% Output : Refutation 110.06s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 18
% Syntax : Number of clauses : 57 ( 37 unt; 0 nHn; 55 RR)
% Number of literals : 92 ( 0 equ; 36 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 11 con; 0-0 aty)
% Number of variables : 59 ( 6 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(meet_a2_and_b2,negated_conjecture,
~ meet(a2,b2,r1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_a2_and_b2) ).
cnf(commutativity_of_meet,axiom,
( ~ meet(X12,X13,X14)
| meet(X13,X12,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_meet) ).
cnf(absorbtion2,axiom,
( ~ join(X35,X36,X37)
| meet(X35,X37,X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorbtion2) ).
cnf(join_r1_and_d,negated_conjecture,
join(r1,d,b2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_r1_and_d) ).
cnf(c63,plain,
meet(r1,b2,r1),
inference(resolution,[status(thm)],[join_r1_and_d,absorbtion2]) ).
cnf(join_r1_and_e,negated_conjecture,
join(r1,e,a2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_r1_and_e) ).
cnf(join_x_and_0,axiom,
join(X5,n0,X5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_x_and_0) ).
cnf(modularity2,axiom,
( ~ meet(X76,X74,X76)
| ~ join(X76,X75,X73)
| ~ meet(X75,X74,X72)
| ~ join(X76,X72,X77)
| meet(X74,X73,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',modularity2) ).
cnf(c165,plain,
( ~ meet(X636,X635,X636)
| ~ join(X636,X637,X638)
| ~ meet(X637,X635,n0)
| meet(X635,X638,X636) ),
inference(resolution,[status(thm)],[modularity2,join_x_and_0]) ).
cnf(commutativity_of_join,axiom,
( ~ join(X20,X21,X22)
| join(X21,X20,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',commutativity_of_join) ).
cnf(absorbtion1,axiom,
( ~ meet(X28,X29,X30)
| join(X28,X30,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',absorbtion1) ).
cnf(meet_r2_and_b,negated_conjecture,
meet(r2,b,e),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_r2_and_b) ).
cnf(c37,plain,
meet(b,r2,e),
inference(resolution,[status(thm)],[meet_r2_and_b,commutativity_of_meet]) ).
cnf(c108,plain,
join(b,e,b),
inference(resolution,[status(thm)],[c37,absorbtion1]) ).
cnf(c242,plain,
join(e,b,b),
inference(resolution,[status(thm)],[c108,commutativity_of_join]) ).
cnf(c390,plain,
meet(e,b,e),
inference(resolution,[status(thm)],[c242,absorbtion2]) ).
cnf(c545,plain,
meet(b,e,e),
inference(resolution,[status(thm)],[c390,commutativity_of_meet]) ).
cnf(meet_0_and_x,axiom,
meet(n0,X10,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_0_and_x) ).
cnf(associativity_of_meet2,axiom,
( ~ meet(X50,X49,X51)
| ~ meet(X49,X48,X52)
| ~ meet(X51,X48,X53)
| meet(X50,X52,X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet2) ).
cnf(c54,plain,
( ~ meet(X148,X150,n0)
| ~ meet(X150,X149,X151)
| meet(X148,X151,n0) ),
inference(resolution,[status(thm)],[associativity_of_meet2,meet_0_and_x]) ).
cnf(c757,plain,
( ~ meet(X1572,b,n0)
| meet(X1572,e,n0) ),
inference(resolution,[status(thm)],[c54,c545]) ).
cnf(join_a_and_b,negated_conjecture,
join(a,b,c2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',join_a_and_b) ).
cnf(c38,plain,
join(b,a,c2),
inference(resolution,[status(thm)],[join_a_and_b,commutativity_of_join]) ).
cnf(c115,plain,
meet(b,c2,b),
inference(resolution,[status(thm)],[c38,absorbtion2]) ).
cnf(meet_r2_and_a,negated_conjecture,
meet(r2,a,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_r2_and_a) ).
cnf(c59,plain,
meet(a,r2,d),
inference(resolution,[status(thm)],[meet_r2_and_a,commutativity_of_meet]) ).
cnf(c166,plain,
join(a,d,a),
inference(resolution,[status(thm)],[c59,absorbtion1]) ).
cnf(c292,plain,
join(d,a,a),
inference(resolution,[status(thm)],[c166,commutativity_of_join]) ).
cnf(c429,plain,
meet(d,a,d),
inference(resolution,[status(thm)],[c292,absorbtion2]) ).
cnf(c39,plain,
meet(a,c2,a),
inference(resolution,[status(thm)],[join_a_and_b,absorbtion2]) ).
cnf(associativity_of_meet1,axiom,
( ~ meet(X44,X43,X45)
| ~ meet(X43,X42,X46)
| ~ meet(X44,X46,X47)
| meet(X45,X42,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity_of_meet1) ).
cnf(c24,plain,
( ~ meet(X79,X81,X80)
| ~ meet(X81,X78,X81)
| meet(X80,X78,X80) ),
inference(factor,[status(thm)],[associativity_of_meet1]) ).
cnf(c199,plain,
( ~ meet(X405,a,X406)
| meet(X406,c2,X406) ),
inference(resolution,[status(thm)],[c24,c39]) ).
cnf(c1487,plain,
meet(d,c2,d),
inference(resolution,[status(thm)],[c199,c429]) ).
cnf(c62,plain,
join(d,r1,b2),
inference(resolution,[status(thm)],[join_r1_and_d,commutativity_of_join]) ).
cnf(meet_c2_and_r1,negated_conjecture,
meet(c2,r1,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_c2_and_r1) ).
cnf(c44,plain,
meet(r1,c2,n0),
inference(resolution,[status(thm)],[meet_c2_and_r1,commutativity_of_meet]) ).
cnf(c2398,plain,
( ~ meet(X4305,c2,X4305)
| ~ join(X4305,r1,X4306)
| meet(c2,X4306,X4305) ),
inference(resolution,[status(thm)],[c165,c44]) ).
cnf(c7211,plain,
( ~ meet(d,c2,d)
| meet(c2,b2,d) ),
inference(resolution,[status(thm)],[c2398,c62]) ).
cnf(c7326,plain,
meet(c2,b2,d),
inference(resolution,[status(thm)],[c7211,c1487]) ).
cnf(meet_a_and_b,negated_conjecture,
meet(a,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_a_and_b) ).
cnf(c16,plain,
meet(b,a,c),
inference(resolution,[status(thm)],[meet_a_and_b,commutativity_of_meet]) ).
cnf(meet_c_and_r2,negated_conjecture,
meet(c,r2,n0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',meet_c_and_r2) ).
cnf(c52,plain,
( ~ meet(X141,X142,c)
| ~ meet(X142,r2,X143)
| meet(X141,X143,n0) ),
inference(resolution,[status(thm)],[associativity_of_meet2,meet_c_and_r2]) ).
cnf(c725,plain,
( ~ meet(X1499,a,c)
| meet(X1499,d,n0) ),
inference(resolution,[status(thm)],[c52,c59]) ).
cnf(c4512,plain,
meet(b,d,n0),
inference(resolution,[status(thm)],[c725,c16]) ).
cnf(c4538,plain,
( ~ meet(b,X5545,X5547)
| ~ meet(X5545,X5546,d)
| meet(X5547,X5546,n0) ),
inference(resolution,[status(thm)],[c4512,associativity_of_meet1]) ).
cnf(c9209,plain,
( ~ meet(b,c2,X5553)
| meet(X5553,b2,n0) ),
inference(resolution,[status(thm)],[c4538,c7326]) ).
cnf(c9224,plain,
meet(b,b2,n0),
inference(resolution,[status(thm)],[c9209,c115]) ).
cnf(c9254,plain,
meet(b2,b,n0),
inference(resolution,[status(thm)],[c9224,commutativity_of_meet]) ).
cnf(c9272,plain,
meet(b2,e,n0),
inference(resolution,[status(thm)],[c9254,c757]) ).
cnf(c9335,plain,
meet(e,b2,n0),
inference(resolution,[status(thm)],[c9272,commutativity_of_meet]) ).
cnf(c9353,plain,
( ~ meet(X6780,b2,X6780)
| ~ join(X6780,e,X6781)
| meet(b2,X6781,X6780) ),
inference(resolution,[status(thm)],[c9335,c165]) ).
cnf(c10773,plain,
( ~ meet(r1,b2,r1)
| meet(b2,a2,r1) ),
inference(resolution,[status(thm)],[c9353,join_r1_and_e]) ).
cnf(c10782,plain,
meet(b2,a2,r1),
inference(resolution,[status(thm)],[c10773,c63]) ).
cnf(c10828,plain,
meet(a2,b2,r1),
inference(resolution,[status(thm)],[c10782,commutativity_of_meet]) ).
cnf(c10869,plain,
$false,
inference(resolution,[status(thm)],[c10828,meet_a2_and_b2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14 % Problem : LAT005-2 : TPTP v8.1.2. Released v1.0.0.
% 0.09/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.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 : Wed May 8 13:15:53 EDT 2024
% 0.14/0.36 % CPUTime :
% 110.06/110.25 % Version: 1.5
% 110.06/110.25 % SZS status Unsatisfiable
% 110.06/110.25 % SZS output start CNFRefutation
% See solution above
% 110.06/110.25
% 110.06/110.25 % Initial clauses : 31
% 110.06/110.25 % Processed clauses : 4125
% 110.06/110.25 % Factors computed : 387
% 110.06/110.25 % Resolvents computed: 10495
% 110.06/110.25 % Tautologies deleted: 467
% 110.06/110.25 % Forward subsumed : 5621
% 110.06/110.25 % Backward subsumed : 66
% 110.06/110.25 % -------- CPU Time ---------
% 110.06/110.25 % User time : 109.859 s
% 110.06/110.25 % System time : 0.025 s
% 110.06/110.25 % Total time : 109.884 s
%------------------------------------------------------------------------------