%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP124-6.004 : TPTP v8.1.2. Released v1.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:23:05 EDT 2024
% Result : Unsatisfiable 7.83s 8.05s
% Output : Refutation 7.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 23
% Syntax : Number of clauses : 93 ( 23 unt; 59 nHn; 91 RR)
% Number of literals : 229 ( 0 equ; 39 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 43 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
cnf(product1_idempotence,axiom,
product1(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
cnf(product1_right_cancellation,axiom,
( ~ product1(X19,X17,X18)
| ~ product1(X19,X20,X18)
| equalish(X17,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
cnf(c10,plain,
( ~ product1(X25,X24,X25)
| equalish(X24,X25) ),
inference(resolution,[status(thm)],[product1_right_cancellation,product1_idempotence]) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
cnf(product1_total_function2,axiom,
( ~ product1(X6,X5,X4)
| ~ product1(X6,X5,X7)
| equalish(X4,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function2) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
cnf(product1_left_cancellation,axiom,
( ~ product1(X27,X28,X29)
| ~ product1(X30,X28,X29)
| equalish(X27,X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
cnf(c13,plain,
( ~ product1(X36,X37,X37)
| equalish(X36,X37) ),
inference(resolution,[status(thm)],[product1_left_cancellation,product1_idempotence]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(product1_total_function1,axiom,
( ~ group_element(X16)
| ~ group_element(X15)
| product1(X16,X15,e_1)
| product1(X16,X15,e_2)
| product1(X16,X15,e_3)
| product1(X16,X15,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
cnf(c5,plain,
( ~ group_element(X79)
| product1(X79,e_1,e_1)
| product1(X79,e_1,e_2)
| product1(X79,e_1,e_3)
| product1(X79,e_1,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_1]) ).
cnf(c42,plain,
( product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c5,element_3]) ).
cnf(c120,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c42,c13]) ).
cnf(c304,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c120,e_3_is_not_e_1]) ).
cnf(c315,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c304,c10]) ).
cnf(c330,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c315,e_1_is_not_e_3]) ).
cnf(c350,plain,
( product1(e_3,e_1,e_4)
| ~ product1(X115,e_1,e_2)
| equalish(X115,e_3) ),
inference(resolution,[status(thm)],[c330,product1_left_cancellation]) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(c43,plain,
( product1(e_4,e_1,e_1)
| product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c5,element_4]) ).
cnf(c159,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c43,c13]) ).
cnf(c660,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c159,e_4_is_not_e_1]) ).
cnf(c680,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c660,c10]) ).
cnf(c693,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c680,e_1_is_not_e_4]) ).
cnf(c710,plain,
( product1(e_4,e_1,e_3)
| product1(e_3,e_1,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c693,c350]) ).
cnf(c770,plain,
( product1(e_4,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c710,e_4_is_not_e_3]) ).
cnf(c790,plain,
( product1(e_4,e_1,e_3)
| ~ product1(e_3,e_1,X170)
| equalish(X170,e_4) ),
inference(resolution,[status(thm)],[c770,product1_total_function2]) ).
cnf(product2_idempotence,axiom,
product2(X3,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
cnf(product2_total_function2,axiom,
( ~ product2(X41,X40,X39)
| ~ product2(X41,X40,X42)
| equalish(X39,X42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
cnf(c21,plain,
( ~ product2(X51,X51,X50)
| equalish(X50,X51) ),
inference(resolution,[status(thm)],[product2_total_function2,product2_idempotence]) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(c41,plain,
( product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c5,element_2]) ).
cnf(c72,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c41,c13]) ).
cnf(c105,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c72,e_2_is_not_e_1]) ).
cnf(c111,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c105,c10]) ).
cnf(c147,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c111,e_1_is_not_e_2]) ).
cnf(c152,plain,
( product1(e_2,e_1,e_3)
| ~ product1(X90,e_1,e_4)
| equalish(X90,e_2) ),
inference(resolution,[status(thm)],[c147,product1_left_cancellation]) ).
cnf(c355,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c330,c152]) ).
cnf(c433,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c355,e_3_is_not_e_2]) ).
cnf(qg2a,negated_conjecture,
( ~ product1(X72,X71,X70)
| ~ product1(X70,X72,X69)
| product2(X69,X71,X72) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
cnf(c6,plain,
( ~ group_element(X80)
| product1(X80,e_2,e_1)
| product1(X80,e_2,e_2)
| product1(X80,e_2,e_3)
| product1(X80,e_2,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_2]) ).
cnf(c46,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c6,element_3]) ).
cnf(c212,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c46,c13]) ).
cnf(c1918,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c212,e_3_is_not_e_2]) ).
cnf(c7317,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1918,c10]) ).
cnf(c7393,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c7317,e_2_is_not_e_3]) ).
cnf(c7427,plain,
( product1(e_3,e_2,e_1)
| ~ product1(X599,e_2,e_4)
| equalish(X599,e_3) ),
inference(resolution,[status(thm)],[c7393,product1_left_cancellation]) ).
cnf(c780,plain,
( product1(e_3,e_1,e_4)
| ~ product1(e_4,e_1,X165)
| equalish(X165,e_3) ),
inference(resolution,[status(thm)],[c770,product1_total_function2]) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
cnf(c466,plain,
( product1(e_3,e_1,e_2)
| ~ product1(X126,e_1,e_3)
| equalish(X126,e_2) ),
inference(resolution,[status(thm)],[c433,product1_left_cancellation]) ).
cnf(c716,plain,
( product1(e_4,e_1,e_2)
| product1(e_3,e_1,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c693,c466]) ).
cnf(c1003,plain,
( product1(e_4,e_1,e_2)
| product1(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c716,e_4_is_not_e_2]) ).
cnf(c1031,plain,
( product1(e_4,e_1,e_2)
| ~ product1(e_1,X239,e_3)
| product2(e_2,X239,e_1) ),
inference(resolution,[status(thm)],[c1003,qg2a]) ).
cnf(c44,plain,
( product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c6,element_1]) ).
cnf(c189,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c44,c10]) ).
cnf(c1279,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c189,e_2_is_not_e_1]) ).
cnf(c1282,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1279,c13]) ).
cnf(c1331,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1282,e_1_is_not_e_2]) ).
cnf(c1332,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2)
| product2(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c1331,c1031]) ).
cnf(c1405,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1332,c21]) ).
cnf(c1442,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c1405,e_1_is_not_e_2]) ).
cnf(c1469,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1442,c780]) ).
cnf(c1792,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1469,e_2_is_not_e_3]) ).
cnf(c1818,plain,
( product1(e_1,e_2,e_4)
| ~ product1(e_3,X371,e_4)
| equalish(X371,e_1) ),
inference(resolution,[status(thm)],[c1792,product1_right_cancellation]) ).
cnf(c7412,plain,
( product1(e_3,e_2,e_1)
| product1(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c7393,c1818]) ).
cnf(c7757,plain,
( product1(e_3,e_2,e_1)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c7412,e_2_is_not_e_1]) ).
cnf(c7789,plain,
( product1(e_3,e_2,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c7757,c7427]) ).
cnf(c7830,plain,
product1(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c7789,e_1_is_not_e_3]) ).
cnf(c7853,plain,
( ~ product1(e_2,X615,e_3)
| product2(e_1,X615,e_2) ),
inference(resolution,[status(thm)],[c7830,qg2a]) ).
cnf(c7897,plain,
( product2(e_1,e_1,e_2)
| product1(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c7853,c433]) ).
cnf(c7916,plain,
( product1(e_3,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c7897,c21]) ).
cnf(c7994,plain,
product1(e_3,e_1,e_2),
inference(resolution,[status(thm)],[c7916,e_2_is_not_e_1]) ).
cnf(c7995,plain,
( product1(e_4,e_1,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c7994,c790]) ).
cnf(c8083,plain,
product1(e_4,e_1,e_3),
inference(resolution,[status(thm)],[c7995,e_2_is_not_e_4]) ).
cnf(c8088,plain,
( ~ product1(e_4,X622,e_3)
| equalish(X622,e_1) ),
inference(resolution,[status(thm)],[c8083,product1_right_cancellation]) ).
cnf(c7849,plain,
( ~ product1(X613,e_2,e_1)
| equalish(X613,e_3) ),
inference(resolution,[status(thm)],[c7830,product1_left_cancellation]) ).
cnf(c47,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c6,element_4]) ).
cnf(c231,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c47,c13]) ).
cnf(c2205,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c231,e_4_is_not_e_2]) ).
cnf(c9108,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2205,c7849]) ).
cnf(c9173,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c9108,e_4_is_not_e_3]) ).
cnf(c9180,plain,
( product1(e_4,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c9173,c8088]) ).
cnf(c9223,plain,
product1(e_4,e_2,e_4),
inference(resolution,[status(thm)],[c9180,e_2_is_not_e_1]) ).
cnf(c9228,plain,
equalish(e_2,e_4),
inference(resolution,[status(thm)],[c9223,c10]) ).
cnf(c9235,plain,
$false,
inference(resolution,[status(thm)],[c9228,e_2_is_not_e_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP124-6.004 : TPTP v8.1.2. Released v1.2.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.34 % Computer : n009.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Thu May 9 03:55:22 EDT 2024
% 0.14/0.34 % CPUTime :
% 7.83/8.05 % Version: 1.5
% 7.83/8.05 % SZS status Unsatisfiable
% 7.83/8.05 % SZS output start CNFRefutation
% See solution above
% 7.83/8.06
% 7.83/8.06 % Initial clauses : 27
% 7.83/8.06 % Processed clauses : 635
% 7.83/8.06 % Factors computed : 9
% 7.83/8.06 % Resolvents computed: 9227
% 7.83/8.06 % Tautologies deleted: 0
% 7.83/8.06 % Forward subsumed : 1948
% 7.83/8.06 % Backward subsumed : 333
% 7.83/8.06 % -------- CPU Time ---------
% 7.83/8.06 % User time : 7.660 s
% 7.83/8.06 % System time : 0.046 s
% 7.83/8.06 % Total time : 7.706 s
%------------------------------------------------------------------------------