%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GRP026-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:37:29 PM UTC 2026
% Result : Unsatisfiable 0.15s 0.61s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 38
% Number of leaves : 28
% Syntax : Number of clauses : 116 ( 59 unt; 48 nHn; 116 RR)
% Number of literals : 261 ( 171 equ; 41 neg)
% Maximal clause size : 7 ( 2 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-4 aty)
% Number of functors : 12 ( 12 usr; 11 con; 0-1 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(all_of_group1,hypothesis,
( ~ group_member(X1,g1)
| X1 = c
| X1 = b
| X1 = a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',all_of_group1) ).
cnf(prove_product_holds_in_group2,negated_conjecture,
~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_product_holds_in_group2) ).
cnf(d3_in_group1,hypothesis,
group_member(d3,g1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_in_group1) ).
cnf(a_maps_to_f,hypothesis,
an_isomorphism(a) = f,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_maps_to_f) ).
cnf(d2_in_group1,hypothesis,
group_member(d2,g1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d2_in_group1) ).
cnf(d1_in_group1,hypothesis,
group_member(d1,g1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_in_group1) ).
cnf(d1_times_d2_is_d3,hypothesis,
product(g1,d1,d2,d3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d1_times_d2_is_d3) ).
cnf(f_times_f_is_f,hypothesis,
product(g2,f,f,f),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_times_f_is_f) ).
cnf(total_function2,axiom,
( ~ product(X1,X2,X3,X5)
| ~ product(X1,X2,X3,X4)
| X5 = X4 ),
file('/export/starexec/sandbox/benchmark/Axioms/GRP006-0.ax',total_function2) ).
cnf(a_times_a_is_a,hypothesis,
product(g1,a,a,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_a_is_a) ).
cnf(c_maps_to_h,hypothesis,
an_isomorphism(c) = h,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_maps_to_h) ).
cnf(a_times_c_is_c,hypothesis,
product(g1,a,c,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_c_is_c) ).
cnf(f_times_h_is_h,hypothesis,
product(g2,f,h,h),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_times_h_is_h) ).
cnf(b_maps_to_g,hypothesis,
an_isomorphism(b) = g,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_maps_to_g) ).
cnf(a_times_b_is_b,hypothesis,
product(g1,a,b,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_b_is_b) ).
cnf(f_times_g_is_g,hypothesis,
product(g2,f,g,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',f_times_g_is_g) ).
cnf(c_times_a_is_c,hypothesis,
product(g1,c,a,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_times_a_is_c) ).
cnf(h_times_f_is_h,hypothesis,
product(g2,h,f,h),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_times_f_is_h) ).
cnf(c_times_c_is_b,hypothesis,
product(g1,c,c,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_times_c_is_b) ).
cnf(h_times_h_is_g,hypothesis,
product(g2,h,h,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_times_h_is_g) ).
cnf(c_times_b_is_a,hypothesis,
product(g1,c,b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c_times_b_is_a) ).
cnf(h_times_g_is_f,hypothesis,
product(g2,h,g,f),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',h_times_g_is_f) ).
cnf(b_times_a_is_b,hypothesis,
product(g1,b,a,b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_times_a_is_b) ).
cnf(g_times_f_is_g,hypothesis,
product(g2,g,f,g),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',g_times_f_is_g) ).
cnf(b_times_c_is_a,hypothesis,
product(g1,b,c,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_times_c_is_a) ).
cnf(g_times_h_is_f,hypothesis,
product(g2,g,h,f),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',g_times_h_is_f) ).
cnf(b_times_b_is_c,hypothesis,
product(g1,b,b,c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_times_b_is_c) ).
cnf(g_times_g_is_h,hypothesis,
product(g2,g,g,h),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',g_times_g_is_h) ).
cnf(c_0_28,hypothesis,
( ~ group_member(X1,g1)
| X1 = c
| X1 = b
| X1 = a ),
inference(fof_simplification,[status(thm)],[all_of_group1]) ).
cnf(c_0_29,negated_conjecture,
~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)),
inference(fof_simplification,[status(thm)],[prove_product_holds_in_group2]) ).
cnf(c_0_30,hypothesis,
( ~ group_member(X1,g1)
| X1 = c
| X1 = b
| X1 = a ),
c_0_28 ).
cnf(c_0_31,hypothesis,
group_member(d3,g1),
d3_in_group1 ).
cnf(c_0_32,negated_conjecture,
~ product(g2,an_isomorphism(d1),an_isomorphism(d2),an_isomorphism(d3)),
c_0_29 ).
cnf(c_0_33,hypothesis,
( d3 = a
| d3 = b
| d3 = c ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_34,hypothesis,
an_isomorphism(a) = f,
a_maps_to_f ).
cnf(c_0_35,hypothesis,
group_member(d2,g1),
d2_in_group1 ).
cnf(c_0_36,negated_conjecture,
( ~ product(g2,an_isomorphism(d1),an_isomorphism(d2),f)
| d3 = c
| d3 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_34]) ).
cnf(c_0_37,hypothesis,
( d2 = a
| d2 = b
| d2 = c ),
inference(spm,[status(thm)],[c_0_30,c_0_35]) ).
cnf(c_0_38,hypothesis,
group_member(d1,g1),
d1_in_group1 ).
cnf(c_0_39,hypothesis,
product(g1,d1,d2,d3),
d1_times_d2_is_d3 ).
cnf(c_0_40,hypothesis,
( ~ product(g2,an_isomorphism(d1),f,f)
| d3 = b
| d3 = c
| d2 = c
| d2 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_36,c_0_37]),c_0_34]) ).
cnf(c_0_41,hypothesis,
( d1 = a
| d1 = b
| d1 = c ),
inference(spm,[status(thm)],[c_0_30,c_0_38]) ).
cnf(c_0_42,hypothesis,
product(g2,f,f,f),
f_times_f_is_f ).
cnf(c_0_43,plain,
( ~ product(X1,X2,X3,X5)
| ~ product(X1,X2,X3,X4)
| X5 = X4 ),
inference(fof_simplification,[status(thm)],[total_function2]) ).
cnf(c_0_44,hypothesis,
( product(g1,d1,a,d3)
| d2 = c
| d2 = b ),
inference(spm,[status(thm)],[c_0_39,c_0_37]) ).
cnf(c_0_45,hypothesis,
( d2 = b
| d2 = c
| d3 = c
| d3 = b
| d1 = c
| d1 = b ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_40,c_0_41]),c_0_34]),c_0_42])]) ).
cnf(c_0_46,plain,
( ~ product(X1,X2,X3,X5)
| ~ product(X1,X2,X3,X4)
| X5 = X4 ),
c_0_43 ).
cnf(c_0_47,hypothesis,
( product(g1,d1,a,c)
| d2 = b
| d2 = c
| d1 = b
| d1 = c
| d3 = b ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_48,hypothesis,
( ~ product(g1,d1,a,X1)
| X1 = c
| d3 = b
| d1 = c
| d1 = b
| d2 = c
| d2 = b ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_49,hypothesis,
( a != c
| d1 = c
| d1 = b ),
inference(ef,[status(thm)],[c_0_41]) ).
cnf(c_0_50,hypothesis,
( a != b
| d1 = c
| d1 = b ),
inference(ef,[status(thm)],[c_0_41]) ).
cnf(c_0_51,hypothesis,
( ~ product(g1,a,a,X1)
| X1 = c
| d2 = b
| d2 = c
| d3 = b
| d1 = c
| d1 = b ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_48,c_0_41]),c_0_49]),c_0_50]) ).
cnf(c_0_52,hypothesis,
product(g1,a,a,a),
a_times_a_is_a ).
cnf(c_0_53,hypothesis,
( d1 = b
| d1 = c
| d3 = b
| d2 = c
| d2 = b ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_51,c_0_52]),c_0_49]) ).
cnf(c_0_54,hypothesis,
( product(g1,d1,a,b)
| d2 = b
| d2 = c
| d1 = c
| d1 = b ),
inference(spm,[status(thm)],[c_0_44,c_0_53]) ).
cnf(c_0_55,hypothesis,
( ~ product(g1,d1,a,X1)
| X1 = b
| d1 = b
| d1 = c
| d2 = c
| d2 = b ),
inference(spm,[status(thm)],[c_0_46,c_0_54]) ).
cnf(c_0_56,hypothesis,
( ~ product(g1,d1,d2,X1)
| X1 = d3 ),
inference(spm,[status(thm)],[c_0_46,c_0_39]) ).
cnf(c_0_57,hypothesis,
( ~ product(g1,a,a,X1)
| X1 = b
| d2 = b
| d2 = c
| d1 = c
| d1 = b ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_41]),c_0_50]),c_0_49]) ).
cnf(c_0_58,hypothesis,
( ~ product(g1,a,d2,X1)
| X1 = d3
| d1 = c
| d1 = b ),
inference(spm,[status(thm)],[c_0_56,c_0_41]) ).
cnf(c_0_59,hypothesis,
( d1 = b
| d1 = c
| d2 = c
| d2 = b ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_52]),c_0_50]) ).
cnf(c_0_60,negated_conjecture,
( ~ product(g2,f,an_isomorphism(d2),an_isomorphism(d3))
| d1 = c
| d1 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_41]),c_0_34]) ).
cnf(c_0_61,hypothesis,
an_isomorphism(c) = h,
c_maps_to_h ).
cnf(c_0_62,hypothesis,
( ~ product(g1,a,c,X1)
| X1 = d3
| d1 = b
| d1 = c
| d2 = b ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_63,hypothesis,
product(g1,a,c,c),
a_times_c_is_c ).
cnf(c_0_64,negated_conjecture,
( ~ product(g2,f,h,an_isomorphism(d3))
| d1 = b
| d1 = c
| d2 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_59]),c_0_61]) ).
cnf(c_0_65,hypothesis,
( d2 = b
| d1 = c
| d1 = b
| d3 = c ),
inference(spm,[status(thm)],[c_0_62,c_0_63]) ).
cnf(c_0_66,hypothesis,
product(g2,f,h,h),
f_times_h_is_h ).
cnf(c_0_67,negated_conjecture,
( d2 = b
| d1 = c
| d1 = b ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_65]),c_0_61]),c_0_66])]) ).
cnf(c_0_68,hypothesis,
an_isomorphism(b) = g,
b_maps_to_g ).
cnf(c_0_69,hypothesis,
( ~ product(g1,a,b,X1)
| X1 = d3
| d1 = b
| d1 = c ),
inference(spm,[status(thm)],[c_0_58,c_0_67]) ).
cnf(c_0_70,hypothesis,
product(g1,a,b,b),
a_times_b_is_b ).
cnf(c_0_71,negated_conjecture,
( ~ product(g2,f,g,an_isomorphism(d3))
| d1 = b
| d1 = c ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_60,c_0_67]),c_0_68]) ).
cnf(c_0_72,hypothesis,
( d1 = c
| d1 = b
| d3 = b ),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_73,hypothesis,
product(g2,f,g,g),
f_times_g_is_g ).
cnf(c_0_74,hypothesis,
( ~ product(g1,d1,a,X1)
| X1 = d3
| d2 = c
| d2 = b ),
inference(spm,[status(thm)],[c_0_56,c_0_37]) ).
cnf(c_0_75,negated_conjecture,
( d1 = c
| d1 = b ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_71,c_0_72]),c_0_68]),c_0_73])]) ).
cnf(c_0_76,negated_conjecture,
( ~ product(g2,an_isomorphism(d1),f,an_isomorphism(d3))
| d2 = c
| d2 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_37]),c_0_34]) ).
cnf(c_0_77,hypothesis,
( ~ product(g1,c,a,X1)
| X1 = d3
| d2 = b
| d2 = c
| d1 = b ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_78,hypothesis,
product(g1,c,a,c),
c_times_a_is_c ).
cnf(c_0_79,negated_conjecture,
( ~ product(g2,h,f,an_isomorphism(d3))
| d2 = b
| d2 = c
| d1 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_75]),c_0_61]) ).
cnf(c_0_80,hypothesis,
( d1 = b
| d2 = c
| d2 = b
| d3 = c ),
inference(spm,[status(thm)],[c_0_77,c_0_78]) ).
cnf(c_0_81,hypothesis,
product(g2,h,f,h),
h_times_f_is_h ).
cnf(c_0_82,hypothesis,
( ~ product(g1,c,d2,X1)
| X1 = d3
| d1 = b ),
inference(spm,[status(thm)],[c_0_56,c_0_75]) ).
cnf(c_0_83,negated_conjecture,
( d1 = b
| d2 = c
| d2 = b ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_80]),c_0_61]),c_0_81])]) ).
cnf(c_0_84,negated_conjecture,
( ~ product(g2,h,an_isomorphism(d2),an_isomorphism(d3))
| d1 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_75]),c_0_61]) ).
cnf(c_0_85,hypothesis,
( ~ product(g1,c,c,X1)
| X1 = d3
| d1 = b
| d2 = b ),
inference(spm,[status(thm)],[c_0_82,c_0_83]) ).
cnf(c_0_86,hypothesis,
product(g1,c,c,b),
c_times_c_is_b ).
cnf(c_0_87,negated_conjecture,
( ~ product(g2,h,h,an_isomorphism(d3))
| d1 = b
| d2 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_83]),c_0_61]) ).
cnf(c_0_88,hypothesis,
( d2 = b
| d1 = b
| d3 = b ),
inference(spm,[status(thm)],[c_0_85,c_0_86]) ).
cnf(c_0_89,hypothesis,
product(g2,h,h,g),
h_times_h_is_g ).
cnf(c_0_90,negated_conjecture,
( d2 = b
| d1 = b ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_88]),c_0_68]),c_0_89])]) ).
cnf(c_0_91,hypothesis,
( ~ product(g1,c,b,X1)
| X1 = d3
| d1 = b ),
inference(spm,[status(thm)],[c_0_82,c_0_90]) ).
cnf(c_0_92,hypothesis,
product(g1,c,b,a),
c_times_b_is_a ).
cnf(c_0_93,negated_conjecture,
( ~ product(g2,h,g,an_isomorphism(d3))
| d1 = b ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_84,c_0_90]),c_0_68]) ).
cnf(c_0_94,hypothesis,
( d1 = b
| d3 = a ),
inference(spm,[status(thm)],[c_0_91,c_0_92]) ).
cnf(c_0_95,hypothesis,
product(g2,h,g,f),
h_times_g_is_f ).
cnf(c_0_96,negated_conjecture,
d1 = b,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_93,c_0_94]),c_0_34]),c_0_95])]) ).
cnf(c_0_97,hypothesis,
( ~ product(g1,b,a,X1)
| X1 = d3
| d2 = b
| d2 = c ),
inference(rw,[status(thm)],[c_0_74,c_0_96]) ).
cnf(c_0_98,hypothesis,
product(g1,b,a,b),
b_times_a_is_b ).
cnf(c_0_99,hypothesis,
( d2 = c
| d2 = b
| d3 = b ),
inference(spm,[status(thm)],[c_0_97,c_0_98]) ).
cnf(c_0_100,hypothesis,
product(g2,g,f,g),
g_times_f_is_g ).
cnf(c_0_101,hypothesis,
product(g1,b,c,a),
b_times_c_is_a ).
cnf(c_0_102,hypothesis,
product(g1,b,d2,d3),
inference(rw,[status(thm)],[c_0_39,c_0_96]) ).
cnf(c_0_103,negated_conjecture,
( d2 = b
| d2 = c ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_99]),c_0_96]),c_0_68]),c_0_68]),c_0_100])]) ).
cnf(c_0_104,hypothesis,
( ~ product(g1,b,c,X1)
| X1 = a ),
inference(spm,[status(thm)],[c_0_46,c_0_101]) ).
cnf(c_0_105,hypothesis,
( product(g1,b,c,d3)
| d2 = b ),
inference(spm,[status(thm)],[c_0_102,c_0_103]) ).
cnf(c_0_106,negated_conjecture,
( ~ product(g2,g,h,an_isomorphism(d3))
| d2 = b ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_103]),c_0_96]),c_0_68]),c_0_61]) ).
cnf(c_0_107,hypothesis,
( d3 = a
| d2 = b ),
inference(spm,[status(thm)],[c_0_104,c_0_105]) ).
cnf(c_0_108,hypothesis,
product(g2,g,h,f),
g_times_h_is_f ).
cnf(c_0_109,hypothesis,
product(g1,b,b,c),
b_times_b_is_c ).
cnf(c_0_110,negated_conjecture,
d2 = b,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_106,c_0_107]),c_0_34]),c_0_108])]) ).
cnf(c_0_111,hypothesis,
( ~ product(g1,b,b,X1)
| X1 = c ),
inference(spm,[status(thm)],[c_0_46,c_0_109]) ).
cnf(c_0_112,hypothesis,
product(g1,b,b,d3),
inference(rw,[status(thm)],[c_0_102,c_0_110]) ).
cnf(c_0_113,hypothesis,
d3 = c,
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_114,hypothesis,
product(g2,g,g,h),
g_times_g_is_h ).
cnf(c_0_115,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_113]),c_0_96]),c_0_68]),c_0_110]),c_0_68]),c_0_61]),c_0_114])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP026-1 : TPTP v9.3.1. Bugfixed v2.0.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.52 % Computer : n019.cluster.edu
% 0.11/0.52 % Model : x86_64 x86_64
% 0.11/0.52 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.52 % Memory : 8046.5625MB
% 0.11/0.52 % OS : Linux 6.8.0-71-generic
% 0.11/0.52 % CPULimit : 300
% 0.11/0.52 % WCLimit : 300
% 0.11/0.52 % DateTime : Sun Sep 20 19:54:21 UTC 2026
% 0.11/0.52 % CPUTime :
% 0.11/0.52 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.56 Running first-order theorem proving
% 0.11/0.56 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.61 % Version: 3.5.1
% 0.15/0.61 % Preprocessing class: FSMSSMSMSSSNFFN.
% 0.15/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/0.61 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with 1500s (5) cores
% 0.15/0.61 % Starting new_bool_3 with 300s (1) cores
% 0.15/0.61 % Starting new_bool_1 with 300s (1) cores
% 0.15/0.61 % Starting sh5l with 300s (1) cores
% 0.15/0.61 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with pid 783599 completed with status 0
% 0.15/0.61 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI
% 0.15/0.61 % Preprocessing class: FSMSSMSMSSSNFFN.
% 0.15/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/0.61 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with 1500s (5) cores
% 0.15/0.61 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/0.61 % No SInE strategy applied
% 0.15/0.61 % Search class: FGUSM-FFMM31-SFFFFFNN
% 0.15/0.61 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.15/0.61 % Starting SubtermCWHack with 136s (1) cores
% 0.15/0.61 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with 151s (1) cores
% 0.15/0.61 % Starting G-E--_208_C18_F1_SE_CS_SP_PS_S5PRR_S0Y with 136s (1) cores
% 0.15/0.61 % Starting new_bool_3 with 136s (1) cores
% 0.15/0.61 % Starting new_bool_1 with 136s (1) cores
% 0.15/0.61 % G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with pid 783605 completed with status 0
% 0.15/0.61 % Result found by G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI
% 0.15/0.61 % Preprocessing class: FSMSSMSMSSSNFFN.
% 0.15/0.61 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.15/0.61 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with 1500s (5) cores
% 0.15/0.61 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.15/0.61 % No SInE strategy applied
% 0.15/0.61 % Search class: FGUSM-FFMM31-SFFFFFNN
% 0.15/0.61 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.15/0.61 % Starting SubtermCWHack with 136s (1) cores
% 0.15/0.61 % Starting G-E--_207_C18_F1_SE_CS_SP_PI_PS_S2SI with 151s (1) cores
% 0.15/0.61 % Preprocessing time : 0.002 s
% 0.15/0.61 % Presaturation interreduction done
% 0.15/0.61
% 0.15/0.61 % Proof found!
% 0.15/0.61 % SZS status Unsatisfiable
% 0.15/0.61 % SZS output start CNFRefutation
% See solution above
% 0.15/0.61 % Parsed axioms : 45
% 0.15/0.61 % Removed by relevancy pruning/SinE : 0
% 0.15/0.61 % Initial clauses : 45
% 0.15/0.61 % Removed in clause preprocessing : 0
% 0.15/0.61 % Initial clauses in saturation : 45
% 0.15/0.61 % Processed clauses : 332
% 0.15/0.61 % ...of these trivial : 0
% 0.15/0.61 % ...subsumed : 62
% 0.15/0.61 % ...remaining for further processing : 270
% 0.15/0.61 % Other redundant clauses eliminated : 0
% 0.15/0.61 % Clauses deleted for lack of memory : 0
% 0.15/0.61 % Backward-subsumed : 73
% 0.15/0.61 % Backward-rewritten : 41
% 0.15/0.61 % Generated clauses : 868
% 0.15/0.61 % ...of the previous two non-redundant : 814
% 0.15/0.61 % ...aggressively subsumed : 0
% 0.15/0.61 % Contextual simplify-reflections : 6
% 0.15/0.61 % Paramodulations : 851
% 0.15/0.61 % Factorizations : 17
% 0.15/0.61 % NegExts : 0
% 0.15/0.61 % Equation resolutions : 0
% 0.15/0.61 % Disequality decompositions : 0
% 0.15/0.61 % Total rewrite steps : 290
% 0.15/0.61 % ...of those cached : 258
% 0.15/0.61 % Propositional unsat checks : 0
% 0.15/0.61 % Propositional check models : 0
% 0.15/0.61 % Propositional check unsatisfiable : 0
% 0.15/0.61 % Propositional clauses : 0
% 0.15/0.61 % Propositional clauses after purity: 0
% 0.15/0.61 % Propositional unsat core size : 0
% 0.15/0.61 % Propositional preprocessing time : 0.000
% 0.15/0.61 % Propositional encoding time : 0.000
% 0.15/0.61 % Propositional solver time : 0.000
% 0.15/0.61 % Success case prop preproc time : 0.000
% 0.15/0.61 % Success case prop encoding time : 0.000
% 0.15/0.61 % Success case prop solver time : 0.000
% 0.15/0.61 % Current number of processed clauses : 111
% 0.15/0.61 % Positive orientable unit clauses : 65
% 0.15/0.61 % Positive unorientable unit clauses: 0
% 0.15/0.61 % Negative unit clauses : 3
% 0.15/0.61 % Non-unit-clauses : 43
% 0.15/0.61 % Current number of unprocessed clauses: 513
% 0.15/0.61 % ...number of literals in the above : 1406
% 0.15/0.61 % Current number of archived formulas : 0
% 0.15/0.61 % Current number of archived clauses : 159
% 0.15/0.61 % Clause-clause subsumption calls (NU) : 4895
% 0.15/0.61 % Rec. Clause-clause subsumption calls : 1357
% 0.15/0.61 % Non-unit clause-clause subsumptions : 139
% 0.15/0.61 % Unit Clause-clause subsumption calls : 59
% 0.15/0.61 % Rewrite failures with RHS unbound : 0
% 0.15/0.61 % BW rewrite match attempts : 153
% 0.15/0.61 % BW rewrite match successes : 5
% 0.15/0.61 % Condensation attempts : 0
% 0.15/0.61 % Condensation successes : 0
% 0.15/0.61 % Termbank termtop insertions : 11016
% 0.15/0.61 % Search garbage collected termcells : 33
% 0.15/0.61
% 0.15/0.61 % -------------------------------------------------
% 0.15/0.61 % User time : 0.024 s
% 0.15/0.61 % System time : 0.008 s
% 0.15/0.61 % Total time : 0.032 s
% 0.15/0.61 % Maximum resident set size: 3656 pages
% 0.15/0.61
% 0.15/0.61 % -------------------------------------------------
% 0.15/0.61 % User time : 0.096 s
% 0.15/0.61 % System time : 0.021 s
% 0.15/0.61 % Total time : 0.117 s
% 0.15/0.61 % Maximum resident set size: 4608 pages
% 0.15/0.61 % E exiting
%------------------------------------------------------------------------------