%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : GRP124-8.004 : TPTP v9.0.0. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n015.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 : Wed Apr 9 06:25:06 PM UTC 2025
% Result : Unsatisfiable 10.30s 3.57s
% Output : CNFRefutation 10.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 35
% Number of leaves : 24
% Syntax : Number of formulae : 266 ( 128 unt; 0 typ; 0 def)
% Number of atoms : 590 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 514 ( 190 ~; 324 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 165 ( 165 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ product2 > product1 > product > next > greater > equalish > cycle > group_element > #nlpp > e_4 > e_3 > e_2 > e_1 > e_0
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(group_element,type,
group_element: $i > $o ).
tff(greater,type,
greater: ( $i * $i ) > $o ).
tff(cycle,type,
cycle: ( $i * $i ) > $o ).
tff(e_2,type,
e_2: $i ).
tff(product,type,
product: ( $i * $i * $i ) > $o ).
tff(next,type,
next: ( $i * $i ) > $o ).
tff(e_0,type,
e_0: $i ).
tff(product1,type,
product1: ( $i * $i * $i ) > $o ).
tff(e_4,type,
e_4: $i ).
tff(e_3,type,
e_3: $i ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(e_1,type,
e_1: $i ).
tff(product2,type,
product2: ( $i * $i * $i ) > $o ).
tff(f_143,axiom,
~ equalish(e_3,e_2),
file(unknown,unknown) ).
tff(f_137,axiom,
~ equalish(e_2,e_3),
file(unknown,unknown) ).
tff(f_151,axiom,
~ equalish(e_4,e_3),
file(unknown,unknown) ).
tff(f_149,axiom,
~ equalish(e_4,e_2),
file(unknown,unknown) ).
tff(f_125,axiom,
group_element(e_2),
file(unknown,unknown) ).
tff(f_127,axiom,
group_element(e_4),
file(unknown,unknown) ).
tff(f_191,axiom,
! [X] : product1(X,X,X),
file(unknown,unknown) ).
tff(f_165,axiom,
! [X,Y] :
( ~ group_element(X)
| ~ group_element(Y)
| product1(X,Y,e_1)
| product1(X,Y,e_2)
| product1(X,Y,e_3)
| product1(X,Y,e_4) ),
file(unknown,unknown) ).
tff(f_181,axiom,
! [X,W,Y,Z] :
( ~ product1(X,W,Y)
| ~ product1(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_145,axiom,
~ equalish(e_3,e_4),
file(unknown,unknown) ).
tff(f_126,axiom,
group_element(e_3),
file(unknown,unknown) ).
tff(f_189,axiom,
! [W,Y,X,Z] :
( ~ product1(W,Y,X)
| ~ product1(Z,Y,X)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_147,axiom,
~ equalish(e_4,e_1),
file(unknown,unknown) ).
tff(f_131,axiom,
~ equalish(e_1,e_3),
file(unknown,unknown) ).
tff(f_124,axiom,
group_element(e_1),
file(unknown,unknown) ).
tff(f_239,axiom,
! [X,Y,Z1,Z2] :
( ~ product1(X,Y,Z1)
| ~ product1(Z1,X,Z2)
| product2(Z2,Y,X) ),
file(unknown,unknown) ).
tff(f_231,axiom,
! [X] : product2(X,X,X),
file(unknown,unknown) ).
tff(f_213,axiom,
! [X,Y,W,Z] :
( ~ product2(X,Y,W)
| ~ product2(X,Y,Z)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_139,axiom,
~ equalish(e_2,e_4),
file(unknown,unknown) ).
tff(f_141,axiom,
~ equalish(e_3,e_1),
file(unknown,unknown) ).
tff(f_205,axiom,
! [X,Y] :
( ~ group_element(X)
| ~ group_element(Y)
| product2(X,Y,e_1)
| product2(X,Y,e_2)
| product2(X,Y,e_3)
| product2(X,Y,e_4) ),
file(unknown,unknown) ).
tff(f_221,axiom,
! [X,W,Y,Z] :
( ~ product2(X,W,Y)
| ~ product2(X,Z,Y)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_229,axiom,
! [W,Y,X,Z] :
( ~ product2(W,Y,X)
| ~ product2(Z,Y,X)
| equalish(W,Z) ),
file(unknown,unknown) ).
tff(f_133,axiom,
~ equalish(e_1,e_4),
file(unknown,unknown) ).
tff(c_66,plain,
~ equalish(e_3,e_2),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_60,plain,
~ equalish(e_2,e_3),
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_74,plain,
~ equalish(e_4,e_3),
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_72,plain,
~ equalish(e_4,e_2),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_46,plain,
group_element(e_2),
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_50,plain,
group_element(e_4),
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_84,plain,
! [X_35] : product1(X_35,X_35,X_35),
inference(cnfTransformation,[status(thm)],[f_191]) ).
tff(c_389,plain,
! [X_137,Y_138] :
( product1(X_137,Y_138,e_4)
| product1(X_137,Y_138,e_3)
| product1(X_137,Y_138,e_2)
| product1(X_137,Y_138,e_1)
| ~ group_element(Y_138)
| ~ group_element(X_137) ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_80,plain,
! [W_28,Z_30,X_27,Y_29] :
( equalish(W_28,Z_30)
| ~ product1(X_27,Z_30,Y_29)
| ~ product1(X_27,W_28,Y_29) ),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_9886,plain,
! [W_537,Y_538,X_539] :
( equalish(W_537,Y_538)
| ~ product1(X_539,W_537,e_4)
| product1(X_539,Y_538,e_3)
| product1(X_539,Y_538,e_2)
| product1(X_539,Y_538,e_1)
| ~ group_element(Y_538)
| ~ group_element(X_539) ),
inference(resolution,[status(thm)],[c_389,c_80]) ).
tff(c_9891,plain,
! [Y_538] :
( equalish(e_4,Y_538)
| product1(e_4,Y_538,e_3)
| product1(e_4,Y_538,e_2)
| product1(e_4,Y_538,e_1)
| ~ group_element(Y_538)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_84,c_9886]) ).
tff(c_10798,plain,
! [Y_596] :
( equalish(e_4,Y_596)
| product1(e_4,Y_596,e_3)
| product1(e_4,Y_596,e_2)
| product1(e_4,Y_596,e_1)
| ~ group_element(Y_596) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_9891]) ).
tff(c_68,plain,
~ equalish(e_3,e_4),
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_48,plain,
group_element(e_3),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_145,plain,
! [W_88,Z_89,Y_90,X_91] :
( equalish(W_88,Z_89)
| ~ product1(Z_89,Y_90,X_91)
| ~ product1(W_88,Y_90,X_91) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_148,plain,
! [W_88,X_35] :
( equalish(W_88,X_35)
| ~ product1(W_88,X_35,X_35) ),
inference(resolution,[status(thm)],[c_84,c_145]) ).
tff(c_405,plain,
! [X_137] :
( equalish(X_137,e_4)
| product1(X_137,e_4,e_3)
| product1(X_137,e_4,e_2)
| product1(X_137,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(X_137) ),
inference(resolution,[status(thm)],[c_389,c_148]) ).
tff(c_10250,plain,
! [X_573] :
( equalish(X_573,e_4)
| product1(X_573,e_4,e_3)
| product1(X_573,e_4,e_2)
| product1(X_573,e_4,e_1)
| ~ group_element(X_573) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_405]) ).
tff(c_155,plain,
! [W_94,Z_95,X_96,Y_97] :
( equalish(W_94,Z_95)
| ~ product1(X_96,Z_95,Y_97)
| ~ product1(X_96,W_94,Y_97) ),
inference(cnfTransformation,[status(thm)],[f_181]) ).
tff(c_158,plain,
! [W_94,X_35] :
( equalish(W_94,X_35)
| ~ product1(X_35,W_94,X_35) ),
inference(resolution,[status(thm)],[c_84,c_155]) ).
tff(c_10268,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_10250,c_158]) ).
tff(c_10294,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_10268]) ).
tff(c_10295,plain,
( product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_68,c_74,c_10294]) ).
tff(c_10303,plain,
product1(e_3,e_4,e_1),
inference(splitLeft,[status(thm)],[c_10295]) ).
tff(c_76,plain,
! [X_21,Y_22] :
( product1(X_21,Y_22,e_4)
| product1(X_21,Y_22,e_3)
| product1(X_21,Y_22,e_2)
| product1(X_21,Y_22,e_1)
| ~ group_element(Y_22)
| ~ group_element(X_21) ),
inference(cnfTransformation,[status(thm)],[f_165]) ).
tff(c_70,plain,
~ equalish(e_4,e_1),
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_54,plain,
~ equalish(e_1,e_3),
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_44,plain,
group_element(e_1),
inference(cnfTransformation,[status(thm)],[f_124]) ).
tff(c_6434,plain,
! [W_406,Y_407,X_408] :
( equalish(W_406,Y_407)
| ~ product1(X_408,W_406,e_4)
| product1(X_408,Y_407,e_3)
| product1(X_408,Y_407,e_2)
| product1(X_408,Y_407,e_1)
| ~ group_element(Y_407)
| ~ group_element(X_408) ),
inference(resolution,[status(thm)],[c_389,c_80]) ).
tff(c_6439,plain,
! [Y_407] :
( equalish(e_4,Y_407)
| product1(e_4,Y_407,e_3)
| product1(e_4,Y_407,e_2)
| product1(e_4,Y_407,e_1)
| ~ group_element(Y_407)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_84,c_6434]) ).
tff(c_9701,plain,
! [Y_534] :
( equalish(e_4,Y_534)
| product1(e_4,Y_534,e_3)
| product1(e_4,Y_534,e_2)
| product1(e_4,Y_534,e_1)
| ~ group_element(Y_534) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_6439]) ).
tff(c_9307,plain,
! [X_519] :
( equalish(X_519,e_4)
| product1(X_519,e_4,e_3)
| product1(X_519,e_4,e_2)
| product1(X_519,e_4,e_1)
| ~ group_element(X_519) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_405]) ).
tff(c_9326,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_9307,c_158]) ).
tff(c_9356,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_9326]) ).
tff(c_9357,plain,
( product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_68,c_74,c_9356]) ).
tff(c_9365,plain,
product1(e_3,e_4,e_1),
inference(splitLeft,[status(thm)],[c_9357]) ).
tff(c_96,plain,
! [Z2_54,Y_52,X_51,Z1_53] :
( product2(Z2_54,Y_52,X_51)
| ~ product1(Z1_53,X_51,Z2_54)
| ~ product1(X_51,Y_52,Z1_53) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_9512,plain,
! [Y_526] :
( product2(e_1,Y_526,e_4)
| ~ product1(e_4,Y_526,e_3) ),
inference(resolution,[status(thm)],[c_9365,c_96]) ).
tff(c_94,plain,
! [X_50] : product2(X_50,X_50,X_50),
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_115,plain,
! [W_70,Z_71,X_72,Y_73] :
( equalish(W_70,Z_71)
| ~ product2(X_72,Y_73,Z_71)
| ~ product2(X_72,Y_73,W_70) ),
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_118,plain,
! [W_70,X_50] :
( equalish(W_70,X_50)
| ~ product2(X_50,X_50,W_70) ),
inference(resolution,[status(thm)],[c_94,c_115]) ).
tff(c_9531,plain,
( equalish(e_4,e_1)
| ~ product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c_9512,c_118]) ).
tff(c_9559,plain,
~ product1(e_4,e_1,e_3),
inference(negUnitSimplification,[status(thm)],[c_70,c_9531]) ).
tff(c_9713,plain,
( equalish(e_4,e_1)
| product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_1)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_9701,c_9559]) ).
tff(c_9745,plain,
( equalish(e_4,e_1)
| product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_9713]) ).
tff(c_9746,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_70,c_9745]) ).
tff(c_9771,plain,
product1(e_4,e_1,e_1),
inference(splitLeft,[status(thm)],[c_9746]) ).
tff(c_62,plain,
~ equalish(e_2,e_4),
inference(cnfTransformation,[status(thm)],[f_139]) ).
tff(c_4008,plain,
! [W_322,Y_323,X_324] :
( equalish(W_322,Y_323)
| ~ product1(X_324,W_322,e_4)
| product1(X_324,Y_323,e_3)
| product1(X_324,Y_323,e_2)
| product1(X_324,Y_323,e_1)
| ~ group_element(Y_323)
| ~ group_element(X_324) ),
inference(resolution,[status(thm)],[c_389,c_80]) ).
tff(c_4013,plain,
! [Y_323] :
( equalish(e_4,Y_323)
| product1(e_4,Y_323,e_3)
| product1(e_4,Y_323,e_2)
| product1(e_4,Y_323,e_1)
| ~ group_element(Y_323)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_84,c_4008]) ).
tff(c_4017,plain,
! [Y_323] :
( equalish(e_4,Y_323)
| product1(e_4,Y_323,e_3)
| product1(e_4,Y_323,e_2)
| product1(e_4,Y_323,e_1)
| ~ group_element(Y_323) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_4013]) ).
tff(c_5561,plain,
! [X_373] :
( equalish(X_373,e_4)
| product1(X_373,e_4,e_3)
| product1(X_373,e_4,e_2)
| product1(X_373,e_4,e_1)
| ~ group_element(X_373) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_405]) ).
tff(c_5586,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_5561,c_158]) ).
tff(c_5623,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_5586]) ).
tff(c_5624,plain,
( product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_68,c_74,c_5623]) ).
tff(c_5632,plain,
product1(e_3,e_4,e_1),
inference(splitLeft,[status(thm)],[c_5624]) ).
tff(c_82,plain,
! [W_31,Z_34,Y_32,X_33] :
( equalish(W_31,Z_34)
| ~ product1(Z_34,Y_32,X_33)
| ~ product1(W_31,Y_32,X_33) ),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_1830,plain,
! [W_240,X_241,Y_242] :
( equalish(W_240,X_241)
| ~ product1(W_240,Y_242,e_4)
| product1(X_241,Y_242,e_3)
| product1(X_241,Y_242,e_2)
| product1(X_241,Y_242,e_1)
| ~ group_element(Y_242)
| ~ group_element(X_241) ),
inference(resolution,[status(thm)],[c_389,c_82]) ).
tff(c_1835,plain,
! [X_241] :
( equalish(e_4,X_241)
| product1(X_241,e_4,e_3)
| product1(X_241,e_4,e_2)
| product1(X_241,e_4,e_1)
| ~ group_element(e_4)
| ~ group_element(X_241) ),
inference(resolution,[status(thm)],[c_84,c_1830]) ).
tff(c_1839,plain,
! [X_241] :
( equalish(e_4,X_241)
| product1(X_241,e_4,e_3)
| product1(X_241,e_4,e_2)
| product1(X_241,e_4,e_1)
| ~ group_element(X_241) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_1835]) ).
tff(c_2361,plain,
! [X_265] :
( equalish(X_265,e_4)
| product1(X_265,e_4,e_3)
| product1(X_265,e_4,e_2)
| product1(X_265,e_4,e_1)
| ~ group_element(X_265) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_405]) ).
tff(c_2377,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_2361,c_158]) ).
tff(c_2403,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_2377]) ).
tff(c_2404,plain,
( product1(e_3,e_4,e_2)
| product1(e_3,e_4,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_68,c_74,c_2403]) ).
tff(c_2412,plain,
product1(e_3,e_4,e_1),
inference(splitLeft,[status(thm)],[c_2404]) ).
tff(c_64,plain,
~ equalish(e_3,e_1),
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_338,plain,
! [X_135,Y_136] :
( product2(X_135,Y_136,e_4)
| product2(X_135,Y_136,e_3)
| product2(X_135,Y_136,e_2)
| product2(X_135,Y_136,e_1)
| ~ group_element(Y_136)
| ~ group_element(X_135) ),
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_135,plain,
! [W_82,Z_83,X_84,Y_85] :
( equalish(W_82,Z_83)
| ~ product2(X_84,Z_83,Y_85)
| ~ product2(X_84,W_82,Y_85) ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_138,plain,
! [W_82,X_50] :
( equalish(W_82,X_50)
| ~ product2(X_50,W_82,X_50) ),
inference(resolution,[status(thm)],[c_94,c_135]) ).
tff(c_349,plain,
! [Y_136] :
( equalish(Y_136,e_4)
| product2(e_4,Y_136,e_3)
| product2(e_4,Y_136,e_2)
| product2(e_4,Y_136,e_1)
| ~ group_element(Y_136)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_338,c_138]) ).
tff(c_1330,plain,
! [Y_211] :
( equalish(Y_211,e_4)
| product2(e_4,Y_211,e_3)
| product2(e_4,Y_211,e_2)
| product2(e_4,Y_211,e_1)
| ~ group_element(Y_211) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_349]) ).
tff(c_105,plain,
! [W_63,Z_64,Y_65,X_66] :
( equalish(W_63,Z_64)
| ~ product2(Z_64,Y_65,X_66)
| ~ product2(W_63,Y_65,X_66) ),
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_108,plain,
! [W_63,X_50] :
( equalish(W_63,X_50)
| ~ product2(W_63,X_50,X_50) ),
inference(resolution,[status(thm)],[c_94,c_105]) ).
tff(c_1346,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product2(e_4,e_3,e_2)
| product2(e_4,e_3,e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_1330,c_108]) ).
tff(c_1362,plain,
( equalish(e_4,e_3)
| equalish(e_3,e_4)
| product2(e_4,e_3,e_2)
| product2(e_4,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_1346]) ).
tff(c_1363,plain,
( product2(e_4,e_3,e_2)
| product2(e_4,e_3,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_68,c_74,c_1362]) ).
tff(c_1365,plain,
product2(e_4,e_3,e_1),
inference(splitLeft,[status(thm)],[c_1363]) ).
tff(c_165,plain,
! [Z2_100,Y_101,X_102,Z1_103] :
( product2(Z2_100,Y_101,X_102)
| ~ product1(Z1_103,X_102,Z2_100)
| ~ product1(X_102,Y_101,Z1_103) ),
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_169,plain,
! [X_104,Y_105] :
( product2(X_104,Y_105,X_104)
| ~ product1(X_104,Y_105,X_104) ),
inference(resolution,[status(thm)],[c_84,c_165]) ).
tff(c_92,plain,
! [W_46,Z_49,Y_47,X_48] :
( equalish(W_46,Z_49)
| ~ product2(Z_49,Y_47,X_48)
| ~ product2(W_46,Y_47,X_48) ),
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_196,plain,
! [W_46,X_104,Y_105] :
( equalish(W_46,X_104)
| ~ product2(W_46,Y_105,X_104)
| ~ product1(X_104,Y_105,X_104) ),
inference(resolution,[status(thm)],[c_169,c_92]) ).
tff(c_1367,plain,
( equalish(e_4,e_1)
| ~ product1(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[c_1365,c_196]) ).
tff(c_1378,plain,
~ product1(e_1,e_3,e_1),
inference(negUnitSimplification,[status(thm)],[c_70,c_1367]) ).
tff(c_56,plain,
~ equalish(e_1,e_4),
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_88,plain,
! [W_40,Z_41,X_38,Y_39] :
( equalish(W_40,Z_41)
| ~ product2(X_38,Y_39,Z_41)
| ~ product2(X_38,Y_39,W_40) ),
inference(cnfTransformation,[status(thm)],[f_213]) ).
tff(c_192,plain,
! [W_40,X_104,Y_105] :
( equalish(W_40,X_104)
| ~ product2(X_104,Y_105,W_40)
| ~ product1(X_104,Y_105,X_104) ),
inference(resolution,[status(thm)],[c_169,c_88]) ).
tff(c_1369,plain,
( equalish(e_1,e_4)
| ~ product1(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c_1365,c_192]) ).
tff(c_1381,plain,
~ product1(e_4,e_3,e_4),
inference(negUnitSimplification,[status(thm)],[c_56,c_1369]) ).
tff(c_1387,plain,
( product1(e_4,e_3,e_3)
| product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_76,c_1381]) ).
tff(c_1390,plain,
( product1(e_4,e_3,e_3)
| product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_1387]) ).
tff(c_1490,plain,
product1(e_4,e_3,e_1),
inference(splitLeft,[status(thm)],[c_1390]) ).
tff(c_1549,plain,
! [Y_225] :
( product2(e_1,Y_225,e_3)
| ~ product1(e_3,Y_225,e_4) ),
inference(resolution,[status(thm)],[c_1490,c_96]) ).
tff(c_1559,plain,
( equalish(e_3,e_1)
| ~ product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c_1549,c_118]) ).
tff(c_1577,plain,
~ product1(e_3,e_1,e_4),
inference(negUnitSimplification,[status(thm)],[c_64,c_1559]) ).
tff(c_1585,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1)
| ~ group_element(e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_76,c_1577]) ).
tff(c_1588,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_44,c_1585]) ).
tff(c_1665,plain,
product1(e_3,e_1,e_1),
inference(splitLeft,[status(thm)],[c_1588]) ).
tff(c_1684,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c_1665,c_148]) ).
tff(c_1698,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64,c_1684]) ).
tff(c_1699,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3) ),
inference(splitRight,[status(thm)],[c_1588]) ).
tff(c_1701,plain,
product1(e_3,e_1,e_3),
inference(splitLeft,[status(thm)],[c_1699]) ).
tff(c_90,plain,
! [W_43,Z_45,X_42,Y_44] :
( equalish(W_43,Z_45)
| ~ product2(X_42,Z_45,Y_44)
| ~ product2(X_42,W_43,Y_44) ),
inference(cnfTransformation,[status(thm)],[f_221]) ).
tff(c_197,plain,
! [W_106,Y_107,X_108] :
( equalish(W_106,Y_107)
| ~ product2(X_108,W_106,X_108)
| ~ product1(X_108,Y_107,X_108) ),
inference(resolution,[status(thm)],[c_169,c_90]) ).
tff(c_203,plain,
! [X_50,Y_107] :
( equalish(X_50,Y_107)
| ~ product1(X_50,Y_107,X_50) ),
inference(resolution,[status(thm)],[c_94,c_197]) ).
tff(c_1770,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c_1701,c_203]) ).
tff(c_1789,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64,c_1770]) ).
tff(c_1790,plain,
product1(e_3,e_1,e_2),
inference(splitRight,[status(thm)],[c_1699]) ).
tff(c_1846,plain,
! [Y_244] :
( product2(e_2,Y_244,e_1)
| ~ product1(e_1,Y_244,e_3) ),
inference(resolution,[status(thm)],[c_1790,c_96]) ).
tff(c_1384,plain,
! [W_46] :
( equalish(W_46,e_4)
| ~ product2(W_46,e_3,e_1) ),
inference(resolution,[status(thm)],[c_1365,c_92]) ).
tff(c_1850,plain,
( equalish(e_2,e_4)
| ~ product1(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c_1846,c_1384]) ).
tff(c_1871,plain,
~ product1(e_1,e_3,e_3),
inference(negUnitSimplification,[status(thm)],[c_62,c_1850]) ).
tff(c_2880,plain,
! [Y_284,Y_285,X_286] :
( product2(e_4,Y_284,Y_285)
| ~ product1(Y_285,Y_284,X_286)
| product1(X_286,Y_285,e_3)
| product1(X_286,Y_285,e_2)
| product1(X_286,Y_285,e_1)
| ~ group_element(Y_285)
| ~ group_element(X_286) ),
inference(resolution,[status(thm)],[c_389,c_96]) ).
tff(c_2882,plain,
( product2(e_4,e_4,e_3)
| product1(e_1,e_3,e_3)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_2412,c_2880]) ).
tff(c_2901,plain,
( product2(e_4,e_4,e_3)
| product1(e_1,e_3,e_3)
| product1(e_1,e_3,e_2)
| product1(e_1,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_48,c_2882]) ).
tff(c_2902,plain,
( product2(e_4,e_4,e_3)
| product1(e_1,e_3,e_2) ),
inference(negUnitSimplification,[status(thm)],[c_1378,c_1871,c_2901]) ).
tff(c_2925,plain,
product1(e_1,e_3,e_2),
inference(splitLeft,[status(thm)],[c_2902]) ).
tff(c_2991,plain,
! [Y_290] :
( product2(e_2,Y_290,e_3)
| ~ product1(e_3,Y_290,e_1) ),
inference(resolution,[status(thm)],[c_2925,c_96]) ).
tff(c_1882,plain,
! [W_40,Y_244] :
( equalish(W_40,e_1)
| ~ product2(e_2,Y_244,W_40)
| ~ product1(e_1,Y_244,e_3) ),
inference(resolution,[status(thm)],[c_1846,c_88]) ).
tff(c_2996,plain,
! [Y_290] :
( equalish(e_3,e_1)
| ~ product1(e_1,Y_290,e_3)
| ~ product1(e_3,Y_290,e_1) ),
inference(resolution,[status(thm)],[c_2991,c_1882]) ).
tff(c_3448,plain,
! [Y_299] :
( ~ product1(e_1,Y_299,e_3)
| ~ product1(e_3,Y_299,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_64,c_2996]) ).
tff(c_3456,plain,
~ product1(e_1,e_4,e_3),
inference(resolution,[status(thm)],[c_2412,c_3448]) ).
tff(c_3463,plain,
( equalish(e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_1)
| ~ group_element(e_1) ),
inference(resolution,[status(thm)],[c_1839,c_3456]) ).
tff(c_3469,plain,
( equalish(e_4,e_1)
| product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_44,c_3463]) ).
tff(c_3470,plain,
( product1(e_1,e_4,e_2)
| product1(e_1,e_4,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_70,c_3469]) ).
tff(c_3475,plain,
product1(e_1,e_4,e_1),
inference(splitLeft,[status(thm)],[c_3470]) ).
tff(c_2429,plain,
! [W_31] :
( equalish(W_31,e_3)
| ~ product1(W_31,e_4,e_1) ),
inference(resolution,[status(thm)],[c_2412,c_82]) ).
tff(c_3568,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c_3475,c_2429]) ).
tff(c_3592,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_54,c_3568]) ).
tff(c_3593,plain,
product1(e_1,e_4,e_2),
inference(splitRight,[status(thm)],[c_3470]) ).
tff(c_2946,plain,
! [W_28] :
( equalish(W_28,e_3)
| ~ product1(e_1,W_28,e_2) ),
inference(resolution,[status(thm)],[c_2925,c_80]) ).
tff(c_3597,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_3593,c_2946]) ).
tff(c_3613,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_3597]) ).
tff(c_3614,plain,
product2(e_4,e_4,e_3),
inference(splitRight,[status(thm)],[c_2902]) ).
tff(c_3709,plain,
( equalish(e_3,e_4)
| ~ product1(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c_3614,c_192]) ).
tff(c_3731,plain,
equalish(e_3,e_4),
inference(demodulation,[status(thm),theory(equality)],[c_84,c_3709]) ).
tff(c_3733,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_68,c_3731]) ).
tff(c_3734,plain,
product1(e_3,e_4,e_2),
inference(splitRight,[status(thm)],[c_2404]) ).
tff(c_1807,plain,
! [W_28] :
( equalish(W_28,e_1)
| ~ product1(e_3,W_28,e_2) ),
inference(resolution,[status(thm)],[c_1790,c_80]) ).
tff(c_3738,plain,
equalish(e_4,e_1),
inference(resolution,[status(thm)],[c_3734,c_1807]) ).
tff(c_3752,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70,c_3738]) ).
tff(c_3753,plain,
( product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_3) ),
inference(splitRight,[status(thm)],[c_1390]) ).
tff(c_3755,plain,
product1(e_4,e_3,e_3),
inference(splitLeft,[status(thm)],[c_3753]) ).
tff(c_3778,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_3755,c_148]) ).
tff(c_3792,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_3778]) ).
tff(c_3793,plain,
product1(e_4,e_3,e_2),
inference(splitRight,[status(thm)],[c_3753]) ).
tff(c_3839,plain,
! [Y_308] :
( product2(e_2,Y_308,e_3)
| ~ product1(e_3,Y_308,e_4) ),
inference(resolution,[status(thm)],[c_3793,c_96]) ).
tff(c_3849,plain,
( equalish(e_3,e_2)
| ~ product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c_3839,c_118]) ).
tff(c_3867,plain,
~ product1(e_3,e_2,e_4),
inference(negUnitSimplification,[status(thm)],[c_66,c_3849]) ).
tff(c_3875,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_76,c_3867]) ).
tff(c_3878,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_46,c_3875]) ).
tff(c_3969,plain,
product1(e_3,e_2,e_1),
inference(splitLeft,[status(thm)],[c_3878]) ).
tff(c_3985,plain,
! [W_28] :
( equalish(W_28,e_2)
| ~ product1(e_3,W_28,e_1) ),
inference(resolution,[status(thm)],[c_3969,c_80]) ).
tff(c_5637,plain,
equalish(e_4,e_2),
inference(resolution,[status(thm)],[c_5632,c_3985]) ).
tff(c_5655,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72,c_5637]) ).
tff(c_5656,plain,
product1(e_3,e_4,e_2),
inference(splitRight,[status(thm)],[c_5624]) ).
tff(c_5815,plain,
! [Y_378] :
( product2(e_2,Y_378,e_4)
| ~ product1(e_4,Y_378,e_3) ),
inference(resolution,[status(thm)],[c_5656,c_96]) ).
tff(c_5834,plain,
( equalish(e_4,e_2)
| ~ product1(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c_5815,c_118]) ).
tff(c_5862,plain,
~ product1(e_4,e_2,e_3),
inference(negUnitSimplification,[status(thm)],[c_72,c_5834]) ).
tff(c_5873,plain,
( equalish(e_4,e_2)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_4017,c_5862]) ).
tff(c_5880,plain,
( equalish(e_4,e_2)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_5873]) ).
tff(c_5881,plain,
( product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_72,c_5880]) ).
tff(c_6011,plain,
product1(e_4,e_2,e_1),
inference(splitLeft,[status(thm)],[c_5881]) ).
tff(c_3986,plain,
! [W_31] :
( equalish(W_31,e_3)
| ~ product1(W_31,e_2,e_1) ),
inference(resolution,[status(thm)],[c_3969,c_82]) ).
tff(c_6017,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_6011,c_3986]) ).
tff(c_6035,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_6017]) ).
tff(c_6036,plain,
product1(e_4,e_2,e_2),
inference(splitRight,[status(thm)],[c_5881]) ).
tff(c_3810,plain,
! [W_28] :
( equalish(W_28,e_3)
| ~ product1(e_4,W_28,e_2) ),
inference(resolution,[status(thm)],[c_3793,c_80]) ).
tff(c_6042,plain,
equalish(e_2,e_3),
inference(resolution,[status(thm)],[c_6036,c_3810]) ).
tff(c_6063,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60,c_6042]) ).
tff(c_6064,plain,
( product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3) ),
inference(splitRight,[status(thm)],[c_3878]) ).
tff(c_6066,plain,
product1(e_3,e_2,e_3),
inference(splitLeft,[status(thm)],[c_6064]) ).
tff(c_6071,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c_6066,c_203]) ).
tff(c_6090,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66,c_6071]) ).
tff(c_6091,plain,
product1(e_3,e_2,e_2),
inference(splitRight,[status(thm)],[c_6064]) ).
tff(c_6111,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c_6091,c_148]) ).
tff(c_6125,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66,c_6111]) ).
tff(c_6126,plain,
product2(e_4,e_3,e_2),
inference(splitRight,[status(thm)],[c_1363]) ).
tff(c_6131,plain,
( equalish(e_2,e_4)
| ~ product1(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c_6126,c_192]) ).
tff(c_6143,plain,
~ product1(e_4,e_3,e_4),
inference(negUnitSimplification,[status(thm)],[c_62,c_6131]) ).
tff(c_6149,plain,
( product1(e_4,e_3,e_3)
| product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_1)
| ~ group_element(e_3)
| ~ group_element(e_4) ),
inference(resolution,[status(thm)],[c_76,c_6143]) ).
tff(c_6152,plain,
( product1(e_4,e_3,e_3)
| product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_50,c_48,c_6149]) ).
tff(c_6209,plain,
product1(e_4,e_3,e_1),
inference(splitLeft,[status(thm)],[c_6152]) ).
tff(c_6219,plain,
! [W_28] :
( equalish(W_28,e_3)
| ~ product1(e_4,W_28,e_1) ),
inference(resolution,[status(thm)],[c_6209,c_80]) ).
tff(c_9778,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c_9771,c_6219]) ).
tff(c_9801,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_54,c_9778]) ).
tff(c_9802,plain,
product1(e_4,e_1,e_2),
inference(splitRight,[status(thm)],[c_9746]) ).
tff(c_6248,plain,
! [Y_394] :
( product2(e_1,Y_394,e_3)
| ~ product1(e_3,Y_394,e_4) ),
inference(resolution,[status(thm)],[c_6209,c_96]) ).
tff(c_6258,plain,
( equalish(e_3,e_1)
| ~ product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c_6248,c_118]) ).
tff(c_6276,plain,
~ product1(e_3,e_1,e_4),
inference(negUnitSimplification,[status(thm)],[c_64,c_6258]) ).
tff(c_6284,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1)
| ~ group_element(e_1)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_76,c_6276]) ).
tff(c_6287,plain,
( product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_44,c_6284]) ).
tff(c_6393,plain,
product1(e_3,e_1,e_1),
inference(splitLeft,[status(thm)],[c_6287]) ).
tff(c_6400,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c_6393,c_148]) ).
tff(c_6410,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64,c_6400]) ).
tff(c_6411,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3) ),
inference(splitRight,[status(thm)],[c_6287]) ).
tff(c_6413,plain,
product1(e_3,e_1,e_3),
inference(splitLeft,[status(thm)],[c_6411]) ).
tff(c_6416,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c_6413,c_203]) ).
tff(c_6431,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64,c_6416]) ).
tff(c_6432,plain,
product1(e_3,e_1,e_2),
inference(splitRight,[status(thm)],[c_6411]) ).
tff(c_6454,plain,
! [W_31] :
( equalish(W_31,e_3)
| ~ product1(W_31,e_1,e_2) ),
inference(resolution,[status(thm)],[c_6432,c_82]) ).
tff(c_9820,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_9802,c_6454]) ).
tff(c_9840,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_9820]) ).
tff(c_9841,plain,
product1(e_3,e_4,e_2),
inference(splitRight,[status(thm)],[c_9357]) ).
tff(c_6453,plain,
! [W_28] :
( equalish(W_28,e_1)
| ~ product1(e_3,W_28,e_2) ),
inference(resolution,[status(thm)],[c_6432,c_80]) ).
tff(c_9847,plain,
equalish(e_4,e_1),
inference(resolution,[status(thm)],[c_9841,c_6453]) ).
tff(c_9863,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_70,c_9847]) ).
tff(c_9864,plain,
( product1(e_4,e_3,e_2)
| product1(e_4,e_3,e_3) ),
inference(splitRight,[status(thm)],[c_6152]) ).
tff(c_9866,plain,
product1(e_4,e_3,e_3),
inference(splitLeft,[status(thm)],[c_9864]) ).
tff(c_9873,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_9866,c_148]) ).
tff(c_9883,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_9873]) ).
tff(c_9884,plain,
product1(e_4,e_3,e_2),
inference(splitRight,[status(thm)],[c_9864]) ).
tff(c_9934,plain,
! [Y_543] :
( product2(e_2,Y_543,e_3)
| ~ product1(e_3,Y_543,e_4) ),
inference(resolution,[status(thm)],[c_9884,c_96]) ).
tff(c_9944,plain,
( equalish(e_3,e_2)
| ~ product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c_9934,c_118]) ).
tff(c_9962,plain,
~ product1(e_3,e_2,e_4),
inference(negUnitSimplification,[status(thm)],[c_66,c_9944]) ).
tff(c_9970,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1)
| ~ group_element(e_2)
| ~ group_element(e_3) ),
inference(resolution,[status(thm)],[c_76,c_9962]) ).
tff(c_9973,plain,
( product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_48,c_46,c_9970]) ).
tff(c_10064,plain,
product1(e_3,e_2,e_1),
inference(splitLeft,[status(thm)],[c_9973]) ).
tff(c_10074,plain,
! [W_28] :
( equalish(W_28,e_2)
| ~ product1(e_3,W_28,e_1) ),
inference(resolution,[status(thm)],[c_10064,c_80]) ).
tff(c_10306,plain,
equalish(e_4,e_2),
inference(resolution,[status(thm)],[c_10303,c_10074]) ).
tff(c_10318,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_72,c_10306]) ).
tff(c_10319,plain,
product1(e_3,e_4,e_2),
inference(splitRight,[status(thm)],[c_10295]) ).
tff(c_10416,plain,
! [Y_580] :
( product2(e_2,Y_580,e_4)
| ~ product1(e_4,Y_580,e_3) ),
inference(resolution,[status(thm)],[c_10319,c_96]) ).
tff(c_10435,plain,
( equalish(e_4,e_2)
| ~ product1(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c_10416,c_118]) ).
tff(c_10463,plain,
~ product1(e_4,e_2,e_3),
inference(negUnitSimplification,[status(thm)],[c_72,c_10435]) ).
tff(c_10809,plain,
( equalish(e_4,e_2)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1)
| ~ group_element(e_2) ),
inference(resolution,[status(thm)],[c_10798,c_10463]) ).
tff(c_10845,plain,
( equalish(e_4,e_2)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1) ),
inference(demodulation,[status(thm),theory(equality)],[c_46,c_10809]) ).
tff(c_10846,plain,
( product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_1) ),
inference(negUnitSimplification,[status(thm)],[c_72,c_10845]) ).
tff(c_10871,plain,
product1(e_4,e_2,e_1),
inference(splitLeft,[status(thm)],[c_10846]) ).
tff(c_10075,plain,
! [W_31] :
( equalish(W_31,e_3)
| ~ product1(W_31,e_2,e_1) ),
inference(resolution,[status(thm)],[c_10064,c_82]) ).
tff(c_10878,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c_10871,c_10075]) ).
tff(c_10898,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_74,c_10878]) ).
tff(c_10899,plain,
product1(e_4,e_2,e_2),
inference(splitRight,[status(thm)],[c_10846]) ).
tff(c_9905,plain,
! [W_28] :
( equalish(W_28,e_3)
| ~ product1(e_4,W_28,e_2) ),
inference(resolution,[status(thm)],[c_9884,c_80]) ).
tff(c_10907,plain,
equalish(e_2,e_3),
inference(resolution,[status(thm)],[c_10899,c_9905]) ).
tff(c_10929,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_60,c_10907]) ).
tff(c_10930,plain,
( product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3) ),
inference(splitRight,[status(thm)],[c_9973]) ).
tff(c_10973,plain,
product1(e_3,e_2,e_3),
inference(splitLeft,[status(thm)],[c_10930]) ).
tff(c_10976,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c_10973,c_203]) ).
tff(c_10991,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66,c_10976]) ).
tff(c_10992,plain,
product1(e_3,e_2,e_2),
inference(splitRight,[status(thm)],[c_10930]) ).
tff(c_11000,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c_10992,c_148]) ).
tff(c_11010,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_66,c_11000]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP124-8.004 : TPTP v9.0.0. Released v1.2.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34 % Computer : n015.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Mon Apr 7 21:20:50 EDT 2025
% 0.13/0.34 % CPUTime :
% 10.30/3.57 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 10.30/3.59
% 10.30/3.59 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------