%------------------------------------------------------------------------------
% File : LisaST---0.9
% Problem : GRP025-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 07:22:07 AM UTC 2026
% Result : Unsatisfiable 31.83s 5.10s
% Output : CNFRefutation 31.83s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 20
% Syntax : Number of clauses : 138 ( 46 unt; 60 nHn; 118 RR)
% Number of literals : 283 ( 147 equ; 69 neg)
% Maximal clause size : 5 ( 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; 9 con; 0-2 aty)
% Number of variables : 115 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(a_and_b_only_members_of_group1,hypothesis,
( X0 = b
| X0 = a
| ~ 'group$umember'(X0,g1) ) ).
cnf(c_and_d_only_members_of_group2,hypothesis,
( X0 = d
| X0 = c
| ~ 'group$umember'(X0,g2) ) ).
cnf(b_times_a_is_b,hypothesis,
product(g1,b,a,b) ).
cnf(b_times_b_is_a,hypothesis,
product(g1,b,b,a) ).
cnf(d_times_d_is_c,hypothesis,
product(g2,d,d,c) ).
cnf(a_maps_to_c,hypothesis,
'an$uisomorphism'(a) = c ).
cnf(b_maps_to_d,hypothesis,
'an$uisomorphism'(b) = d ).
cnf(d1_member_of_group1,hypothesis,
'group$umember'(d1,g1) ).
cnf(d2_member_of_group1,hypothesis,
'group$umember'(d2,g1) ).
cnf(d3_member_of_group1,hypothesis,
'group$umember'(d3,g1) ).
cnf(d1_times_d2_is_d3,hypothesis,
product(g1,d1,d2,d3) ).
cnf(prove_product_holds_in_group2,negated_conjecture,
~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),'an$uisomorphism'(d3)) ).
cnf(identity_in_group,axiom,
'group$umember'('identity$ufor'(X0),X0) ).
cnf(left_identity,axiom,
product(X0,'identity$ufor'(X0),X1,X1) ).
cnf(right_identity,axiom,
product(X0,X1,'identity$ufor'(X0),X1) ).
cnf(left_inverse,axiom,
product(X0,inverse(X0,X1),X1,'identity$ufor'(X0)) ).
cnf(right_inverse,axiom,
product(X0,X1,inverse(X0,X1),'identity$ufor'(X0)) ).
cnf(total_function2,axiom,
( X4 = X3
| ~ product(X0,X1,X2,X4)
| ~ product(X0,X1,X2,X3) ) ).
cnf(associativity1,axiom,
( product(X0,X1,X5,X6)
| ~ product(X0,X3,X4,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ) ).
cnf(associativity2,axiom,
( product(X0,X3,X4,X6)
| ~ product(X0,X1,X5,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ) ).
cnf(c4,plain,
( X0 = b
| X0 = a
| ~ 'group$umember'(X0,g1) ),
inference(clausification,[status(esa)],[a_and_b_only_members_of_group1]) ).
cnf(c5,plain,
( X0 = d
| X0 = c
| ~ 'group$umember'(X0,g2) ),
inference(clausification,[status(esa)],[c_and_d_only_members_of_group2]) ).
cnf(c8,plain,
product(g1,b,a,b),
inference(clausification,[status(esa)],[b_times_a_is_b]) ).
cnf(c9,plain,
product(g1,b,b,a),
inference(clausification,[status(esa)],[b_times_b_is_a]) ).
cnf(c13,plain,
product(g2,d,d,c),
inference(clausification,[status(esa)],[d_times_d_is_c]) ).
cnf(c14,plain,
'an$uisomorphism'(a) = c,
inference(clausification,[status(esa)],[a_maps_to_c]) ).
cnf(c15,plain,
'an$uisomorphism'(b) = d,
inference(clausification,[status(esa)],[b_maps_to_d]) ).
cnf(c16,plain,
'group$umember'(d1,g1),
inference(clausification,[status(esa)],[d1_member_of_group1]) ).
cnf(c17,plain,
'group$umember'(d2,g1),
inference(clausification,[status(esa)],[d2_member_of_group1]) ).
cnf(c18,plain,
'group$umember'(d3,g1),
inference(clausification,[status(esa)],[d3_member_of_group1]) ).
cnf(c19,plain,
product(g1,d1,d2,d3),
inference(clausification,[status(esa)],[d1_times_d2_is_d3]) ).
cnf(c20,plain,
~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),'an$uisomorphism'(d3)),
inference(clausification,[status(esa)],[prove_product_holds_in_group2]) ).
cnf(c21,plain,
'group$umember'('identity$ufor'(X0),X0),
inference(clausification,[status(esa)],[identity_in_group]) ).
cnf(c22,plain,
product(X0,'identity$ufor'(X0),X1,X1),
inference(clausification,[status(esa)],[left_identity]) ).
cnf(c23,plain,
product(X0,X1,'identity$ufor'(X0),X1),
inference(clausification,[status(esa)],[right_identity]) ).
cnf(c25,plain,
product(X0,inverse(X0,X1),X1,'identity$ufor'(X0)),
inference(clausification,[status(esa)],[left_inverse]) ).
cnf(c26,plain,
product(X0,X1,inverse(X0,X1),'identity$ufor'(X0)),
inference(clausification,[status(esa)],[right_inverse]) ).
cnf(c29,plain,
( X4 = X3
| ~ product(X0,X1,X2,X4)
| ~ product(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[total_function2]) ).
cnf(c30,plain,
( product(X0,X1,X5,X6)
| ~ product(X0,X3,X4,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[associativity1]) ).
cnf(c31,plain,
( product(X0,X3,X4,X6)
| ~ product(X0,X1,X5,X6)
| ~ product(X0,X2,X4,X5)
| ~ product(X0,X1,X2,X3) ),
inference(clausification,[status(esa)],[associativity2]) ).
cnf(d0,plain,
( ~ product(X2,'identity$ufor'(X2),X0,X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[c29,c22]) ).
cnf(d1,plain,
( ~ product(g1,b,b,X0)
| a = X0 ),
inference(resolution,[status(thm)],[c29,c9]) ).
cnf(d2,plain,
( 'identity$ufor'(g1) = b
| 'identity$ufor'(g1) = a ),
inference(resolution,[status(thm)],[c4,c21]) ).
cnf(d3,plain,
( 'identity$ufor'(g1) = a
| product(g1,b,X0,X0) ),
inference(superposition,[status(thm)],[d2,c22]) ).
cnf(d4,plain,
( 'identity$ufor'(g1) = a
| product(g1,X0,inverse(g1,X0),b) ),
inference(superposition,[status(thm)],[d2,c26]) ).
cnf(d5,plain,
( 'identity$ufor'(g1) = a
| ~ product(g1,X1,inverse(g1,X1),X0)
| b = X0 ),
inference(resolution,[status(thm)],[c29,d4]) ).
cnf(d6,plain,
( 'identity$ufor'(g1) = a
| 'identity$ufor'(g1) = a
| b = inverse(g1,b) ),
inference(resolution,[status(thm)],[d5,d3]) ).
cnf(d7,plain,
( 'identity$ufor'(g1) = a
| product(g1,b,b,'identity$ufor'(g1)) ),
inference(superposition,[status(thm)],[d6,c26]) ).
cnf(d8,plain,
( a = 'identity$ufor'(g1)
| 'identity$ufor'(g1) = a ),
inference(resolution,[status(thm)],[d7,d1]) ).
cnf(d9,plain,
( a = 'identity$ufor'(g1)
| product(g1,X0,a,X0) ),
inference(superposition,[status(thm)],[d8,c23]) ).
cnf(d10,plain,
( a = 'identity$ufor'(g1)
| a = 'identity$ufor'(g1) ),
inference(resolution,[status(thm)],[d9,d0]) ).
cnf(d11,plain,
( X0 = X1
| ~ product(g1,a,X0,X1) ),
inference(superposition,[status(thm)],[d10,d0]) ).
cnf(d12,plain,
( d3 = b
| d3 = a ),
inference(resolution,[status(thm)],[c4,c18]) ).
cnf(d13,plain,
( d3 = a
| product(g1,d1,d2,b) ),
inference(superposition,[status(thm)],[d12,c19]) ).
cnf(d14,plain,
( d3 = a
| ~ product(g1,d1,d2,X0)
| b = X0 ),
inference(resolution,[status(thm)],[c29,d13]) ).
cnf(d15,plain,
( d3 = a
| b = d3 ),
inference(resolution,[status(thm)],[d14,c19]) ).
cnf(d16,plain,
( b = d3
| product(g1,d1,d2,a) ),
inference(superposition,[status(thm)],[d15,c19]) ).
cnf(d17,plain,
( ~ product(g1,d1,d2,X0)
| a = X0
| b = d3 ),
inference(resolution,[status(thm)],[d16,c29]) ).
cnf(d18,plain,
( b = d3
| a = d3 ),
inference(resolution,[status(thm)],[d17,c19]) ).
cnf(d19,plain,
( a = d3
| ~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),'an$uisomorphism'(b)) ),
inference(superposition,[status(thm)],[d18,c20]) ).
cnf(d20,plain,
( ~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),d)
| a = d3 ),
inference(demodulation,[status(thm)],[d19,c15]) ).
cnf(d21,plain,
( ~ product(X2,X0,'identity$ufor'(X2),X1)
| X0 = X1 ),
inference(resolution,[status(thm)],[c29,c23]) ).
cnf(d22,plain,
( X0 = X1
| ~ product(g1,X0,a,X1) ),
inference(superposition,[status(thm)],[d10,d21]) ).
cnf(d23,plain,
( d2 = b
| d2 = a ),
inference(resolution,[status(thm)],[c4,c17]) ).
cnf(d24,plain,
( d2 = a
| product(g1,d1,b,d3) ),
inference(superposition,[status(thm)],[d23,c19]) ).
cnf(d25,plain,
( d1 = b
| d1 = a ),
inference(resolution,[status(thm)],[c4,c16]) ).
cnf(d26,plain,
( d1 = a
| d2 = a
| product(g1,b,b,d3) ),
inference(superposition,[status(thm)],[d25,d24]) ).
cnf(d27,plain,
( d2 = a
| d1 = a
| a = d3 ),
inference(resolution,[status(thm)],[d1,d26]) ).
cnf(d28,plain,
( d1 = a
| a = d3
| product(g1,d1,a,d3) ),
inference(superposition,[status(thm)],[d27,c19]) ).
cnf(d29,plain,
( d1 = d3
| d1 = a
| a = d3 ),
inference(resolution,[status(thm)],[d28,d22]) ).
cnf(d30,plain,
( d1 = a
| ~ product(g2,'an$uisomorphism'(b),'an$uisomorphism'(d2),'an$uisomorphism'(d3)) ),
inference(superposition,[status(thm)],[d25,c20]) ).
cnf(d31,plain,
( ~ product(g2,d,'an$uisomorphism'(d2),'an$uisomorphism'(d3))
| d1 = a ),
inference(demodulation,[status(thm)],[d30,c15]) ).
cnf(d32,plain,
( d3 = a
| d1 = a
| ~ product(g2,d,'an$uisomorphism'(d2),'an$uisomorphism'(b)) ),
inference(superposition,[status(thm)],[d12,d31]) ).
cnf(d33,plain,
( ~ product(g2,d,'an$uisomorphism'(d2),d)
| d3 = a
| d1 = a ),
inference(demodulation,[status(thm)],[d32,c15]) ).
cnf(d34,plain,
( d1 = a
| a = d3
| d3 = a
| d1 = a
| ~ product(g2,d,'an$uisomorphism'(a),d) ),
inference(superposition,[status(thm)],[d27,d33]) ).
cnf(d35,plain,
( ~ product(g2,d,c,d)
| d3 = a
| d1 = a
| a = d3 ),
inference(demodulation,[status(thm)],[d34,c14]) ).
cnf(d36,plain,
( ~ product(g2,d,d,X0)
| c = X0 ),
inference(resolution,[status(thm)],[c29,c13]) ).
cnf(d37,plain,
( 'identity$ufor'(g2) = d
| 'identity$ufor'(g2) = c ),
inference(resolution,[status(thm)],[c5,c21]) ).
cnf(d38,plain,
( 'identity$ufor'(g2) = c
| product(g2,d,X0,X0) ),
inference(superposition,[status(thm)],[d37,c22]) ).
cnf(d39,plain,
( 'identity$ufor'(g2) = c
| product(g2,X0,inverse(g2,X0),d) ),
inference(superposition,[status(thm)],[d37,c26]) ).
cnf(d40,plain,
( 'identity$ufor'(g2) = c
| ~ product(g2,X1,inverse(g2,X1),X0)
| d = X0 ),
inference(resolution,[status(thm)],[c29,d39]) ).
cnf(d41,plain,
( 'identity$ufor'(g2) = c
| 'identity$ufor'(g2) = c
| d = inverse(g2,d) ),
inference(resolution,[status(thm)],[d40,d38]) ).
cnf(d42,plain,
( 'identity$ufor'(g2) = c
| product(g2,d,d,'identity$ufor'(g2)) ),
inference(superposition,[status(thm)],[d41,c26]) ).
cnf(d43,plain,
( c = 'identity$ufor'(g2)
| 'identity$ufor'(g2) = c ),
inference(resolution,[status(thm)],[d42,d36]) ).
cnf(d44,plain,
( c = 'identity$ufor'(g2)
| product(g2,X0,c,X0) ),
inference(superposition,[status(thm)],[d43,c23]) ).
cnf(d45,plain,
( c = 'identity$ufor'(g2)
| c = 'identity$ufor'(g2) ),
inference(resolution,[status(thm)],[d44,d0]) ).
cnf(d46,plain,
product(g2,X0,c,X0),
inference(superposition,[status(thm)],[d45,c23]) ).
cnf(d47,plain,
( d3 = a
| d1 = a
| a = d3 ),
inference(resolution,[status(thm)],[d46,d35]) ).
cnf(d48,plain,
( d1 = a
| a = d3
| d1 = a
| a = d3
| d1 = a ),
inference(superposition,[status(thm)],[d47,d29]) ).
cnf(d49,plain,
( a = d3
| a = d3
| ~ product(g2,'an$uisomorphism'(a),'an$uisomorphism'(d2),d) ),
inference(superposition,[status(thm)],[d48,d20]) ).
cnf(d50,plain,
( ~ product(g2,c,'an$uisomorphism'(d2),d)
| a = d3 ),
inference(demodulation,[status(thm)],[d49,c14]) ).
cnf(d51,plain,
( ~ product(g1,d1,d2,X0)
| d3 = X0 ),
inference(resolution,[status(thm)],[c29,c19]) ).
cnf(d52,plain,
( a = d3
| product(g1,d1,d2,b) ),
inference(superposition,[status(thm)],[d18,c19]) ).
cnf(d53,plain,
( d3 = b
| a = d3 ),
inference(resolution,[status(thm)],[d52,d51]) ).
cnf(d54,plain,
( a = d3
| product(g1,a,d2,d3) ),
inference(superposition,[status(thm)],[d48,c19]) ).
cnf(d55,plain,
( d2 = d3
| a = d3 ),
inference(resolution,[status(thm)],[d54,d11]) ).
cnf(d56,plain,
( a = d3
| a = d3
| d2 = b ),
inference(superposition,[status(thm)],[d55,d53]) ).
cnf(d57,plain,
( a = d3
| a = d3
| ~ product(g2,c,'an$uisomorphism'(b),d) ),
inference(superposition,[status(thm)],[d56,d50]) ).
cnf(d58,plain,
( ~ product(g2,c,d,d)
| a = d3 ),
inference(demodulation,[status(thm)],[d57,c15]) ).
cnf(d59,plain,
product(g2,c,X0,X0),
inference(superposition,[status(thm)],[d45,c22]) ).
cnf(d60,plain,
a = d3,
inference(resolution,[status(thm)],[d59,d58]) ).
cnf(d61,plain,
( ~ product(g2,d,'an$uisomorphism'(d2),'an$uisomorphism'(a))
| d1 = a ),
inference(demodulation,[status(thm)],[d31,d60]) ).
cnf(d62,plain,
( ~ product(g2,d,'an$uisomorphism'(d2),c)
| d1 = a ),
inference(demodulation,[status(thm)],[d61,c14]) ).
cnf(d63,plain,
( d1 = a
| product(g1,b,d2,d3) ),
inference(superposition,[status(thm)],[d25,c19]) ).
cnf(d64,plain,
product(g1,X0,a,X0),
inference(superposition,[status(thm)],[d10,c23]) ).
cnf(d65,plain,
( product(g1,d1,X2,X1)
| ~ product(g1,d2,X0,X2)
| ~ product(g1,d3,X0,X1) ),
inference(resolution,[status(thm)],[c30,c19]) ).
cnf(d66,plain,
( ~ product(g1,d2,a,X0)
| product(g1,d1,X0,d3) ),
inference(resolution,[status(thm)],[d65,d64]) ).
cnf(d67,plain,
product(g1,inverse(g1,X0),X0,a),
inference(superposition,[status(thm)],[d10,c25]) ).
cnf(d68,plain,
( product(X0,X3,X4,X2)
| ~ product(X0,inverse(X0,X3),X1,X4)
| ~ product(X0,'identity$ufor'(X0),X1,X2) ),
inference(resolution,[status(thm)],[c30,c26]) ).
cnf(d69,plain,
( ~ product(g1,'identity$ufor'(g1),X0,X1)
| product(g1,X0,a,X1) ),
inference(resolution,[status(thm)],[d68,d67]) ).
cnf(d70,plain,
( ~ product(g1,a,X0,X1)
| product(g1,X0,a,X1) ),
inference(demodulation,[status(thm)],[d69,d10]) ).
cnf(d71,plain,
( d1 = a
| d3 = a
| product(g1,b,d2,b) ),
inference(superposition,[status(thm)],[d25,d13]) ).
cnf(d72,plain,
( ~ product(X0,inverse(X0,X4),X3,X1)
| ~ product(X0,X3,X2,X4)
| product(X0,X1,X2,'identity$ufor'(X0)) ),
inference(resolution,[status(thm)],[c31,c25]) ).
cnf(d73,plain,
( product(g1,a,X1,'identity$ufor'(g1))
| ~ product(g1,X0,X1,X0) ),
inference(resolution,[status(thm)],[d72,d67]) ).
cnf(d74,plain,
( product(g1,a,X1,a)
| ~ product(g1,X0,X1,X0) ),
inference(demodulation,[status(thm)],[d73,d10]) ).
cnf(d75,plain,
( d3 = a
| d1 = a
| product(g1,a,d2,a) ),
inference(resolution,[status(thm)],[d74,d71]) ).
cnf(d76,plain,
( product(g1,d2,a,a)
| d3 = a
| d1 = a ),
inference(resolution,[status(thm)],[d75,d70]) ).
cnf(d77,plain,
( product(g1,d1,a,d3)
| d3 = a
| d1 = a ),
inference(resolution,[status(thm)],[d76,d66]) ).
cnf(d78,plain,
( d1 = d3
| d3 = a
| d1 = a ),
inference(resolution,[status(thm)],[d77,d22]) ).
cnf(d79,plain,
( d1 = d3
| d1 = a
| d1 = a
| product(g1,b,d2,a) ),
inference(superposition,[status(thm)],[d78,d63]) ).
cnf(d80,plain,
( ~ product(g1,b,X2,X0)
| ~ product(g1,X2,X1,a)
| product(g1,X0,X1,b) ),
inference(resolution,[status(thm)],[c31,c8]) ).
cnf(d81,plain,
( product(g1,a,X0,b)
| ~ product(g1,b,X0,a) ),
inference(resolution,[status(thm)],[d80,c9]) ).
cnf(d82,plain,
( d1 = d3
| d1 = a
| product(g1,a,d2,b) ),
inference(resolution,[status(thm)],[d81,d79]) ).
cnf(d83,plain,
( d2 = b
| d1 = d3
| d1 = a ),
inference(resolution,[status(thm)],[d82,d11]) ).
cnf(d84,plain,
( d2 = b
| d1 = a
| d1 = a ),
inference(demodulation,[status(thm)],[d83,d60]) ).
cnf(d85,plain,
( d1 = a
| d1 = a
| ~ product(g2,d,'an$uisomorphism'(b),c) ),
inference(superposition,[status(thm)],[d84,d62]) ).
cnf(d86,plain,
( ~ product(g2,d,d,c)
| d1 = a ),
inference(demodulation,[status(thm)],[d85,c15]) ).
cnf(d87,plain,
d1 = a,
inference(resolution,[status(thm)],[c13,d86]) ).
cnf(d88,plain,
product(g1,d1,d2,a),
inference(demodulation,[status(thm)],[c19,d60]) ).
cnf(d89,plain,
product(g1,a,d2,a),
inference(demodulation,[status(thm)],[d88,d87]) ).
cnf(d90,plain,
d2 = a,
inference(resolution,[status(thm)],[d89,d11]) ).
cnf(d91,plain,
~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),'an$uisomorphism'(a)),
inference(demodulation,[status(thm)],[c20,d60]) ).
cnf(d92,plain,
~ product(g2,'an$uisomorphism'(d1),'an$uisomorphism'(d2),c),
inference(demodulation,[status(thm)],[d91,c14]) ).
cnf(d93,plain,
~ product(g2,'an$uisomorphism'(a),'an$uisomorphism'(d2),c),
inference(demodulation,[status(thm)],[d92,d87]) ).
cnf(d94,plain,
~ product(g2,c,'an$uisomorphism'(d2),c),
inference(demodulation,[status(thm)],[d93,c14]) ).
cnf(d95,plain,
~ product(g2,c,'an$uisomorphism'(a),c),
inference(demodulation,[status(thm)],[d94,d90]) ).
cnf(d96,plain,
~ product(g2,c,c,c),
inference(demodulation,[status(thm)],[d95,c14]) ).
cnf(d97,plain,
$false,
inference(resolution,[status(thm)],[d46,d96]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP025-1 : TPTP v9.3.1. Bugfixed v1.2.1.
% 0.00/0.04 % Command : casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n026.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Fri Sep 25 14:19:56 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running casc-portfolio.sh -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 31.83/5.10 % SZS status Unsatisfiable for theBenchmark.p
% 31.83/5.10 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
%------------------------------------------------------------------------------