%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP132-1.002 : 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:14 EDT 2024
% Result : Unsatisfiable 1.78s 1.96s
% Output : Refutation 1.78s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 10
% Syntax : Number of clauses : 53 ( 9 unt; 35 nHn; 53 RR)
% Number of literals : 134 ( 0 equ; 42 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 2 ( 2 usr; 2 con; 0-0 aty)
% Number of variables : 46 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_right_cancellation,axiom,
( ~ product(X13,X14,X11)
| ~ product(X13,X12,X11)
| equalish(X14,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(product_total_function1,axiom,
( ~ group_element(X6)
| ~ group_element(X7)
| product(X6,X7,e_1)
| product(X6,X7,e_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c3,plain,
( ~ group_element(X43)
| product(X43,e_2,e_1)
| product(X43,e_2,e_2) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c47,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2) ),
inference(resolution,[status(thm)],[c3,element_1]) ).
cnf(c119,plain,
( product(e_1,e_2,e_1)
| ~ product(e_1,X122,e_2)
| equalish(X122,e_2) ),
inference(resolution,[status(thm)],[c47,product_right_cancellation]) ).
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(c2,plain,
( ~ group_element(X42)
| product(X42,e_1,e_1)
| product(X42,e_1,e_2) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c46,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c2,element_2]) ).
cnf(product_left_cancellation,axiom,
( ~ product(X21,X18,X20)
| ~ product(X19,X18,X20)
| equalish(X21,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(c1,plain,
( ~ group_element(X35)
| product(X35,X35,e_1)
| product(X35,X35,e_2) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c9,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c1,element_1]) ).
cnf(c15,plain,
( product(e_1,e_1,e_2)
| ~ product(X62,e_1,e_1)
| equalish(X62,e_1) ),
inference(resolution,[status(thm)],[c9,product_left_cancellation]) ).
cnf(c129,plain,
( product(e_1,e_1,e_2)
| equalish(e_2,e_1)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c15,c46]) ).
cnf(c369,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c129,e_2_is_not_e_1]) ).
cnf(c410,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c369,c119]) ).
cnf(c2007,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c410,e_1_is_not_e_2]) ).
cnf(c2063,plain,
( product(e_2,e_1,e_2)
| ~ product(e_1,X288,e_1)
| equalish(X288,e_2) ),
inference(resolution,[status(thm)],[c2007,product_right_cancellation]) ).
cnf(c18,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,X65,e_2)
| equalish(X65,e_1) ),
inference(resolution,[status(thm)],[c9,product_right_cancellation]) ).
cnf(c133,plain,
( product(e_1,e_1,e_1)
| equalish(e_2,e_1)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c18,c47]) ).
cnf(c501,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c133,e_2_is_not_e_1]) ).
cnf(qg2_1,negated_conjecture,
( ~ product(X30,X26,X28)
| ~ product(X27,X29,X28)
| ~ product(X25,X30,X26)
| ~ product(X25,X27,X29)
| equalish(X30,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2_1) ).
cnf(c6,plain,
( ~ product(X49,X50,X48)
| ~ product(X50,X48,X48)
| ~ product(X49,X49,X50)
| equalish(X49,X50) ),
inference(factor,[status(thm)],[qg2_1]) ).
cnf(c78,plain,
( ~ product(e_1,e_2,X157)
| ~ product(e_2,X157,X157)
| equalish(e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c6,c9]) ).
cnf(c22,plain,
( product(e_1,e_1,e_1)
| ~ product(X80,e_1,e_2)
| equalish(X80,e_1) ),
inference(resolution,[status(thm)],[c9,product_left_cancellation]) ).
cnf(c147,plain,
( product(e_1,e_1,e_1)
| equalish(e_2,e_1)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c22,c46]) ).
cnf(c644,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c147,e_2_is_not_e_1]) ).
cnf(c718,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c644,c78]) ).
cnf(c2455,plain,
( product(e_1,e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c718,c501]) ).
cnf(c2469,plain,
( equalish(e_1,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c2455,c2063]) ).
cnf(c2663,plain,
product(e_2,e_1,e_2),
inference(resolution,[status(thm)],[c2469,e_1_is_not_e_2]) ).
cnf(product_total_function2,axiom,
( ~ product(X3,X5,X4)
| ~ product(X3,X5,X2)
| equalish(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c11,plain,
( product(e_1,e_1,e_2)
| ~ product(e_1,X58,e_1)
| equalish(X58,e_1) ),
inference(resolution,[status(thm)],[c9,product_right_cancellation]) ).
cnf(c112,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c47,c11]) ).
cnf(c275,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c112,e_2_is_not_e_1]) ).
cnf(c304,plain,
( product(e_1,e_2,e_2)
| ~ product(e_1,e_1,X155)
| equalish(X155,e_2) ),
inference(resolution,[status(thm)],[c275,product_total_function2]) ).
cnf(c2472,plain,
( equalish(e_1,e_2)
| product(e_1,e_2,e_2) ),
inference(resolution,[status(thm)],[c2455,c304]) ).
cnf(c2741,plain,
product(e_1,e_2,e_2),
inference(resolution,[status(thm)],[c2472,e_1_is_not_e_2]) ).
cnf(qg2_2,negated_conjecture,
( ~ product(X41,X37,X39)
| ~ product(X38,X40,X39)
| ~ product(X36,X41,X37)
| ~ product(X36,X38,X40)
| equalish(X37,X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2_2) ).
cnf(c32,plain,
( ~ product(X78,X79,X77)
| ~ product(X79,X77,X77)
| ~ product(X78,X78,X79)
| equalish(X79,X77) ),
inference(factor,[status(thm)],[qg2_2]) ).
cnf(c10,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c1,element_2]) ).
cnf(c61,plain,
( product(e_2,e_2,e_1)
| ~ product(X99,e_2,e_2)
| equalish(X99,e_2) ),
inference(resolution,[status(thm)],[c10,product_left_cancellation]) ).
cnf(c175,plain,
( product(e_2,e_2,e_1)
| equalish(e_1,e_2)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c61,c47]) ).
cnf(c1329,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c175,e_1_is_not_e_2]) ).
cnf(c1408,plain,
( product(e_2,e_2,e_1)
| ~ product(e_1,X247,e_1)
| equalish(X247,e_2) ),
inference(resolution,[status(thm)],[c1329,product_right_cancellation]) ).
cnf(c2462,plain,
( equalish(e_1,e_2)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c2455,c1408]) ).
cnf(c2576,plain,
product(e_2,e_2,e_1),
inference(resolution,[status(thm)],[c2462,e_1_is_not_e_2]) ).
cnf(c2625,plain,
( ~ product(e_2,e_1,X364)
| ~ product(e_1,X364,X364)
| equalish(e_1,X364) ),
inference(resolution,[status(thm)],[c2576,c32]) ).
cnf(c2820,plain,
( ~ product(e_2,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2625,c2741]) ).
cnf(c2822,plain,
equalish(e_1,e_2),
inference(resolution,[status(thm)],[c2820,c2663]) ).
cnf(c2823,plain,
$false,
inference(resolution,[status(thm)],[c2822,e_1_is_not_e_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP132-1.002 : TPTP v8.1.2. Released v1.2.0.
% 0.07/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:49:53 EDT 2024
% 0.14/0.34 % CPUTime :
% 1.78/1.96 % Version: 1.5
% 1.78/1.96 % SZS status Unsatisfiable
% 1.78/1.96 % SZS output start CNFRefutation
% See solution above
% 1.78/1.96
% 1.78/1.96 % Initial clauses : 10
% 1.78/1.96 % Processed clauses : 216
% 1.78/1.96 % Factors computed : 50
% 1.78/1.96 % Resolvents computed: 2774
% 1.78/1.96 % Tautologies deleted: 8
% 1.78/1.96 % Forward subsumed : 678
% 1.78/1.96 % Backward subsumed : 159
% 1.78/1.96 % -------- CPU Time ---------
% 1.78/1.96 % User time : 1.595 s
% 1.78/1.96 % System time : 0.017 s
% 1.78/1.96 % Total time : 1.612 s
%------------------------------------------------------------------------------