%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : ITP387_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n005.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:55:30 PM UTC 2026
% Result : Theorem 47.79s 17.47s
% Output : CNFRefutation 47.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 9
% Syntax : Number of formulae : 37 ( 33 unt; 0 typ; 0 def)
% Number of atoms : 43 ( 42 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 15 ( 9 ~; 4 |; 1 &)
% ( 1 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 25 ( 25 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 35 ( 35 usr; 11 con; 0-2 aty)
% Number of variables : 78 ( 0 sgn 77 !; 1 ?; 78 :)
% Comments :
%------------------------------------------------------------------------------
tff(decl_sort1,type,
'A_ell2$': $tType ).
tff(decl_sort2,type,
'C$': $tType ).
tff(decl_sort3,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$': $tType ).
tff(decl_sort4,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun$': $tType ).
tff(decl_sort5,type,
'A_c_prod_ell2_b_d_prod_ell2_fun$': $tType ).
tff(decl_sort6,type,
'A_c_prod_ell2$': $tType ).
tff(decl_sort7,type,
'C_ell2$': $tType ).
tff(decl_sort8,type,
'C_ell2_d_ell2_cblinfun$': $tType ).
tff(decl_sort9,type,
'A_c_prod$': $tType ).
tff(decl_sort10,type,
'A$': $tType ).
tff(decl_sort11,type,
'D_ell2$': $tType ).
tff(decl_sort12,type,
'B_d_prod_ell2$': $tType ).
tff(decl_sort13,type,
'A_ell2_b_ell2_cblinfun$': $tType ).
tff(decl_sort14,type,
'A_ell2_b_ell2_fun$': $tType ).
tff(decl_sort15,type,
'C_ell2_d_ell2_fun$': $tType ).
tff(decl_sort16,type,
'B_ell2$': $tType ).
tff(decl_sort17,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$': $tType ).
tff(decl_sort18,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$': $tType ).
tff(decl_sort19,type,
'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$': $tType ).
tff(decl_sort20,type,
'C_a_c_prod_fun$': $tType ).
tff(decl_sort21,type,
'A_c_a_c_prod_fun_fun$': $tType ).
tff(decl_sort22,type,
'C_a_prod$': $tType ).
tff(decl_sort23,type,
'A_c_prod_a_c_prod_ell2_fun$': $tType ).
tff(decl_sort24,type,
'A_c_prod_c_a_prod_fun$': $tType ).
tff(decl_sort25,type,
'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$': $tType ).
tff(decl_29,type,
'fst$e': 'A_c_prod$' > 'A$' ).
tff(decl_44,type,
'cblinfun_apply$': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' ).
tff(decl_60,type,
'fun_app$q': ( 'A$' * 'A_c_a_c_prod_fun_fun$' ) > 'C_a_c_prod_fun$' ).
tff(decl_64,type,
'b2$': 'C_ell2_d_ell2_cblinfun$' ).
tff(decl_72,type,
'fun_app$l': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_fun_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_fun$' ).
tff(decl_73,type,
'tensor_ell2$': ( 'D_ell2$' * 'B_ell2$' ) > 'B_d_prod_ell2$' ).
tff(decl_85,type,
'fun_app$t': ( 'A_ell2$' * 'A_ell2_b_ell2_fun$' ) > 'B_ell2$' ).
tff(decl_89,type,
'fun_app$u': ( 'C_ell2$' * 'C_ell2_d_ell2_fun$' ) > 'D_ell2$' ).
tff(decl_99,type,
'b1$': 'C_ell2_d_ell2_cblinfun$' ).
tff(decl_107,type,
'plus$u': ( 'B_d_prod_ell2$' * 'B_d_prod_ell2$' ) > 'B_d_prod_ell2$' ).
tff(decl_108,type,
'i$': 'A$' ).
tff(decl_115,type,
'snd$e': 'A_c_prod$' > 'C$' ).
tff(decl_119,type,
'ket$': 'A_c_prod_a_c_prod_ell2_fun$' ).
tff(decl_128,type,
'cblinfun_apply$a': 'A_ell2_b_ell2_cblinfun$' > 'A_ell2_b_ell2_fun$' ).
tff(decl_135,type,
'a$': 'A_ell2_b_ell2_cblinfun$' ).
tff(decl_141,type,
'fun_app$s': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' ).
tff(decl_163,type,
'fun_app$m': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ) > 'C_ell2_d_ell2_cblinfun$' ).
tff(decl_184,type,
'plus$a': 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' ).
tff(decl_201,type,
'plus$b': 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun_fun$' ).
tff(decl_202,type,
'fun_app$p': ( 'C$' * 'C_a_c_prod_fun$' ) > 'A_c_prod$' ).
tff(decl_216,type,
'pair$': 'A_c_a_c_prod_fun_fun$' ).
tff(decl_218,type,
'fun_app$n': ( 'C_ell2_d_ell2_cblinfun$' * 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun_fun$' ) > 'C_ell2_d_ell2_cblinfun_c_ell2_d_ell2_cblinfun_fun$' ).
tff(decl_224,type,
'cblinfun_apply$b': 'C_ell2_d_ell2_cblinfun$' > 'C_ell2_d_ell2_fun$' ).
tff(decl_232,type,
'tensor_op$': ( 'C_ell2_d_ell2_cblinfun$' * 'A_ell2_b_ell2_cblinfun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(decl_235,type,
'swap$d': 'A_c_prod_c_a_prod_fun$' ).
tff(decl_269,type,
'fun_app$ah': ( 'A_c_prod$' * 'A_c_prod_c_a_prod_fun$' ) > 'C_a_prod$' ).
tff(decl_270,type,
'fun_app$o': ( 'A_c_prod$' * 'A_c_prod_a_c_prod_ell2_fun$' ) > 'A_c_prod_ell2$' ).
tff(decl_271,type,
'ket$a': 'A$' > 'A_ell2$' ).
tff(decl_283,type,
'plus$i': ( 'D_ell2$' * 'D_ell2$' ) > 'D_ell2$' ).
tff(decl_305,type,
'fun_app$k': ( 'A_c_prod_ell2$' * 'A_c_prod_ell2_b_d_prod_ell2_fun$' ) > 'B_d_prod_ell2$' ).
tff(decl_315,type,
'ket$b': 'C$' > 'C_ell2$' ).
tff(decl_343,type,
'fun_app$r': ( 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' * 'A_c_prod_ell2_b_d_prod_ell2_cblinfun_a_c_prod_ell2_b_d_prod_ell2_cblinfun_fun$' ) > 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$' ).
tff(decl_357,type,
'j$': 'C$' ).
tff(decl_359,type,
'fst$d': 'C_a_prod$' > 'C$' ).
tff(decl_478,type,
esk111_2: ( 'A_c_prod$' * 'C$' ) > 'A$' ).
tff(axiom407,axiom,
! [X1160: 'C$',X1161: 'A_c_prod$'] :
( ( X1160 = 'snd$e'(X1161) )
<=> ? [X1162: 'A$'] : ( X1161 = 'fun_app$p'('fun_app$q'('pair$',X1162),X1160) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom407) ).
tff(axiom430,axiom,
! [X1206: 'A_c_prod$'] : ( 'fst$d'('fun_app$ah'('swap$d',X1206)) = 'snd$e'(X1206) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom430) ).
tff(conjecture9,conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conjecture9) ).
tff(axiom349,axiom,
! [X993: 'A$',X994: 'C$'] : ( 'fst$e'('fun_app$p'('fun_app$q'('pair$',X993),X994)) = X993 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom349) ).
tff(axiom20,axiom,
! [X59: 'A_ell2_b_ell2_cblinfun$',X60: 'C_ell2_d_ell2_cblinfun$',X61: 'A$',X62: 'C$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X59,X60)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X61),X62))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X59),'ket$a'(X61)),'fun_app$u'('cblinfun_apply$b'(X60),'ket$b'(X62))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom20) ).
tff(axiom34,axiom,
! [X111: 'C_ell2_d_ell2_cblinfun$',X112: 'C_ell2_d_ell2_cblinfun$',X113: 'C_ell2$'] : ( 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X111),X112)),X113) = 'plus$i'('fun_app$u'('cblinfun_apply$b'(X111),X113),'fun_app$u'('cblinfun_apply$b'(X112),X113)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom34) ).
tff(axiom35,axiom,
! [X114: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X115: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X116: 'A_c_prod_ell2$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X114),X115)),X116) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X114),X116),'fun_app$k'('fun_app$l'('cblinfun_apply$',X115),X116)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom35) ).
tff(axiom337,axiom,
! [X964: 'A$',X965: 'C$'] : ( 'snd$e'('fun_app$p'('fun_app$q'('pair$',X964),X965)) = X965 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom337) ).
tff(axiom95,axiom,
! [X293: 'B_ell2$',X294: 'D_ell2$',X295: 'D_ell2$'] : ( 'tensor_ell2$'(X293,'plus$i'(X294,X295)) = 'plus$u'('tensor_ell2$'(X293,X294),'tensor_ell2$'(X293,X295)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom95) ).
tff(c_0_9,plain,
! [X2987: 'C$',X2988: 'A_c_prod$',X2990: 'C$',X2991: 'A_c_prod$',X2992: 'A$'] :
( ( ( X2990 = 'snd$e'(X2991) )
| ( X2991 != 'fun_app$p'('fun_app$q'('pair$',X2992),X2990) ) )
& ( ( X2988 = 'fun_app$p'('fun_app$q'('pair$',esk111_2(X2987,X2988)),X2987) )
| ( X2987 != 'snd$e'(X2988) ) ) ),
inference(fof_nnf,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom407])])])])])]) ).
tff(c_0_10,plain,
! [X3057: 'A_c_prod$'] : ( 'fst$d'('fun_app$ah'('swap$d',X3057)) = 'snd$e'(X3057) ),
inference(variable_rename,[status(thm)],[axiom430]) ).
tff(c_0_11,negated_conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(assume_negation,[status(cth)],[conjecture9]) ).
tcf(c_0_12,plain,
! [X62: 'C$',X4: 'A_c_prod$'] :
( ( X62 != 'snd$e'(X4) )
| ( X4 = 'fun_app$p'('fun_app$q'('pair$',esk111_2(X62,X4)),X62) ) ),
inference(split_conjunct,[status(thm)],[c_0_9]) ).
tcf(c_0_13,plain,
! [X4: 'A_c_prod$'] : 'fst$d'('fun_app$ah'('swap$d',X4)) = 'snd$e'(X4),
inference(split_conjunct,[status(thm)],[c_0_10]) ).
tff(c_0_14,negated_conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(fof_simplification,[status(thm)],[c_0_11]) ).
tff(c_0_15,plain,
! [X2773: 'A$',X2774: 'C$'] : ( 'fst$e'('fun_app$p'('fun_app$q'('pair$',X2773),X2774)) = X2773 ),
inference(variable_rename,[status(thm)],[axiom349]) ).
tcf(c_0_16,plain,
! [X62: 'C$',X4: 'A_c_prod$'] :
( ( X62 != 'fst$d'('fun_app$ah'('swap$d',X4)) )
| ( X4 = 'fun_app$p'('fun_app$q'('pair$',esk111_2(X62,X4)),X62) ) ),
inference(rw,[status(thm)],[c_0_12,c_0_13]) ).
tff(c_0_17,negated_conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(fof_nnf,[status(thm)],[c_0_14]) ).
tff(c_0_18,plain,
! [X1777: 'A_ell2_b_ell2_cblinfun$',X1778: 'C_ell2_d_ell2_cblinfun$',X1779: 'A$',X1780: 'C$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X1777,X1778)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X1779),X1780))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X1777),'ket$a'(X1779)),'fun_app$u'('cblinfun_apply$b'(X1778),'ket$b'(X1780))) ),
inference(variable_rename,[status(thm)],[axiom20]) ).
tff(c_0_19,plain,
! [X1829: 'C_ell2_d_ell2_cblinfun$',X1830: 'C_ell2_d_ell2_cblinfun$',X1831: 'C_ell2$'] : ( 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X1829),X1830)),X1831) = 'plus$i'('fun_app$u'('cblinfun_apply$b'(X1829),X1831),'fun_app$u'('cblinfun_apply$b'(X1830),X1831)) ),
inference(variable_rename,[status(thm)],[axiom34]) ).
tff(c_0_20,plain,
! [X1832: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1833: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X1834: 'A_c_prod_ell2$'] : ( 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X1832),X1833)),X1834) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X1832),X1834),'fun_app$k'('fun_app$l'('cblinfun_apply$',X1833),X1834)) ),
inference(variable_rename,[status(thm)],[axiom35]) ).
tcf(c_0_21,plain,
! [X62: 'C$',X10: 'A$'] : 'fst$e'('fun_app$p'('fun_app$q'('pair$',X10),X62)) = X10,
inference(split_conjunct,[status(thm)],[c_0_15]) ).
tcf(c_0_22,plain,
! [X4: 'A_c_prod$'] : 'fun_app$p'('fun_app$q'('pair$',esk111_2('fst$d'('fun_app$ah'('swap$d',X4)),X4)),'fst$d'('fun_app$ah'('swap$d',X4))) = X4,
inference(er,[status(thm)],[c_0_16]) ).
tff(c_0_23,plain,
! [X2743: 'A$',X2744: 'C$'] : ( 'snd$e'('fun_app$p'('fun_app$q'('pair$',X2743),X2744)) = X2744 ),
inference(variable_rename,[status(thm)],[axiom337]) ).
tcf(c_0_24,negated_conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'('a$','fun_app$m'('fun_app$n'('plus$a','b1$'),'b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
tcf(c_0_25,plain,
! [X10: 'A$',X13: 'C_ell2_d_ell2_cblinfun$',X59: 'A_ell2_b_ell2_cblinfun$',X62: 'C$'] : 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X59,X13)),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X10),X62))) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X59),'ket$a'(X10)),'fun_app$u'('cblinfun_apply$b'(X13),'ket$b'(X62))),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
tcf(c_0_26,plain,
! [X13: 'C_ell2_d_ell2_cblinfun$',X14: 'C_ell2_d_ell2_cblinfun$',X113: 'C_ell2$'] : 'fun_app$u'('cblinfun_apply$b'('fun_app$m'('fun_app$n'('plus$a',X13),X14)),X113) = 'plus$i'('fun_app$u'('cblinfun_apply$b'(X13),X113),'fun_app$u'('cblinfun_apply$b'(X14),X113)),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
tcf(c_0_27,plain,
! [X12: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X11: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X8: 'A_c_prod_ell2$'] : 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X11),X12)),X8) = 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X11),X8),'fun_app$k'('fun_app$l'('cblinfun_apply$',X12),X8)),
inference(split_conjunct,[status(thm)],[c_0_20]) ).
tcf(c_0_28,plain,
! [X4: 'A_c_prod$'] : esk111_2('fst$d'('fun_app$ah'('swap$d',X4)),X4) = 'fst$e'(X4),
inference(spm,[status(thm)],[c_0_21,c_0_22]) ).
tcf(c_0_29,plain,
! [X10: 'A$',X62: 'C$'] : 'snd$e'('fun_app$p'('fun_app$q'('pair$',X10),X62)) = X62,
inference(split_conjunct,[status(thm)],[c_0_23]) ).
tff(c_0_30,plain,
! [X2018: 'B_ell2$',X2019: 'D_ell2$',X2020: 'D_ell2$'] : ( 'tensor_ell2$'(X2018,'plus$i'(X2019,X2020)) = 'plus$u'('tensor_ell2$'(X2018,X2019),'tensor_ell2$'(X2018,X2020)) ),
inference(variable_rename,[status(thm)],[axiom95]) ).
tcf(c_0_31,negated_conjecture,
'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b','tensor_op$'('a$','b1$')),'tensor_op$'('a$','b2$'))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$','i$'),'j$'))) != 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'('a$'),'ket$a'('i$')),'plus$i'('fun_app$u'('cblinfun_apply$b'('b1$'),'ket$b'('j$')),'fun_app$u'('cblinfun_apply$b'('b2$'),'ket$b'('j$')))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_24,c_0_25]),c_0_26]) ).
tcf(c_0_32,plain,
! [X10: 'A$',X13: 'C_ell2_d_ell2_cblinfun$',X59: 'A_ell2_b_ell2_cblinfun$',X11: 'A_c_prod_ell2_b_d_prod_ell2_cblinfun$',X62: 'C$'] : 'plus$u'('fun_app$k'('fun_app$l'('cblinfun_apply$',X11),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X10),X62))),'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X59),'ket$a'(X10)),'fun_app$u'('cblinfun_apply$b'(X13),'ket$b'(X62)))) = 'fun_app$k'('fun_app$l'('cblinfun_apply$','fun_app$r'('fun_app$s'('plus$b',X11),'tensor_op$'(X59,X13))),'fun_app$o'('ket$','fun_app$p'('fun_app$q'('pair$',X10),X62))),
inference(spm,[status(thm)],[c_0_27,c_0_25]) ).
tcf(c_0_33,plain,
! [X59: 'A_ell2_b_ell2_cblinfun$',X13: 'C_ell2_d_ell2_cblinfun$',X4: 'A_c_prod$'] : 'fun_app$k'('fun_app$l'('cblinfun_apply$','tensor_op$'(X59,X13)),'fun_app$o'('ket$',X4)) = 'tensor_ell2$'('fun_app$t'('cblinfun_apply$a'(X59),'ket$a'('fst$e'(X4))),'fun_app$u'('cblinfun_apply$b'(X13),'ket$b'('fst$d'('fun_app$ah'('swap$d',X4))))),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_25,c_0_22]),c_0_28]) ).
tcf(c_0_34,plain,
! [X10: 'A$',X62: 'C$'] : 'fst$d'('fun_app$ah'('swap$d','fun_app$p'('fun_app$q'('pair$',X10),X62))) = X62,
inference(rw,[status(thm)],[c_0_29,c_0_13]) ).
tcf(c_0_35,plain,
! [X39: 'D_ell2$',X281: 'B_ell2$',X41: 'D_ell2$'] : 'tensor_ell2$'(X281,'plus$i'(X39,X41)) = 'plus$u'('tensor_ell2$'(X281,X39),'tensor_ell2$'(X281,X41)),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_36,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)],[c_0_31,c_0_32]),c_0_33]),c_0_21]),c_0_34]),c_0_35])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP387_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.05 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/10.40 % Computer : n005.cluster.edu
% 0.13/10.40 % Model : x86_64 x86_64
% 0.13/10.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/10.40 % Memory : 8046.5625MB
% 0.13/10.40 % OS : Linux 6.8.0-71-generic
% 0.13/10.41 % CPULimit : 300
% 0.13/10.41 % WCLimit : 300
% 0.13/10.41 % DateTime : Sun Sep 20 22:36:29 UTC 2026
% 0.13/10.41 % CPUTime :
% 0.13/10.41 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/10.44 Running first-order theorem proving
% 0.13/10.44 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
% 47.79/17.47 % Version: 3.5.1
% 47.79/17.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 47.79/17.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 47.79/17.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 47.79/17.47 % Starting new_bool_3 with 300s (1) cores
% 47.79/17.47 % Starting new_bool_1 with 300s (1) cores
% 47.79/17.47 % Starting sh5l with 300s (1) cores
% 47.79/17.47 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 1903968 completed with status 0
% 47.79/17.47 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 47.79/17.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 47.79/17.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 47.79/17.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 47.79/17.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 47.79/17.47 % No SInE strategy applied
% 47.79/17.47 % Search class: FGHSM-FSLM31-DFFFFFNN
% 47.79/17.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 47.79/17.47 % Starting SubtermCWHack with 136s (1) cores
% 47.79/17.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 47.79/17.47 % Starting C07_19_nc_SAT001_MinMin_p005000_rr with 354s (1) cores
% 47.79/17.47 % Starting U----_206c_10_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 47.79/17.47 % Starting G-E--_302_C18_F1_URBAN_S5PRR_RG_S0Y with 136s (1) cores
% 47.79/17.47 % U----_206c_10_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with pid 1903978 completed with status 0
% 47.79/17.47 % Result found by U----_206c_10_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN
% 47.79/17.47 % Preprocessing class: FMLMSMSMSSSNFFN.
% 47.79/17.47 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 47.79/17.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 47.79/17.47 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 47.79/17.47 % No SInE strategy applied
% 47.79/17.47 % Search class: FGHSM-FSLM31-DFFFFFNN
% 47.79/17.47 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 47.79/17.47 % Starting SubtermCWHack with 136s (1) cores
% 47.79/17.47 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 47.79/17.47 % Starting C07_19_nc_SAT001_MinMin_p005000_rr with 354s (1) cores
% 47.79/17.47 % Starting U----_206c_10_B11_00_F1_SE_PI_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 47.79/17.47 % Preprocessing time : 0.013 s
% 47.79/17.47 % Presaturation interreduction done
% 47.79/17.47
% 47.79/17.47 % Proof found!
% 47.79/17.47 % SZS status Theorem
% 47.79/17.47 % SZS output start CNFRefutation
% See solution above
% 47.79/17.47 % Parsed axioms : 1134
% 47.79/17.47 % Removed by relevancy pruning/SinE : 0
% 47.79/17.47 % Initial clauses : 1396
% 47.79/17.47 % Removed in clause preprocessing : 605
% 47.79/17.47 % Initial clauses in saturation : 791
% 47.79/17.47 % Processed clauses : 19415
% 47.79/17.47 % ...of these trivial : 831
% 47.79/17.47 % ...subsumed : 14980
% 47.79/17.47 % ...remaining for further processing : 3604
% 47.79/17.47 % Other redundant clauses eliminated : 13974
% 47.79/17.47 % Clauses deleted for lack of memory : 0
% 47.79/17.47 % Backward-subsumed : 107
% 47.79/17.47 % Backward-rewritten : 166
% 47.79/17.47 % Generated clauses : 308991
% 47.79/17.47 % ...of the previous two non-redundant : 279941
% 47.79/17.47 % ...aggressively subsumed : 0
% 47.79/17.47 % Contextual simplify-reflections : 0
% 47.79/17.47 % Paramodulations : 294812
% 47.79/17.47 % Factorizations : 0
% 47.79/17.47 % NegExts : 0
% 47.79/17.47 % Equation resolutions : 14183
% 47.79/17.47 % Disequality decompositions : 0
% 47.79/17.47 % Total rewrite steps : 158665
% 47.79/17.47 % ...of those cached : 135749
% 47.79/17.47 % Propositional unsat checks : 0
% 47.79/17.47 % Propositional check models : 0
% 47.79/17.47 % Propositional check unsatisfiable : 0
% 47.79/17.47 % Propositional clauses : 0
% 47.79/17.47 % Propositional clauses after purity: 0
% 47.79/17.47 % Propositional unsat core size : 0
% 47.79/17.47 % Propositional preprocessing time : 0.000
% 47.79/17.47 % Propositional encoding time : 0.000
% 47.79/17.47 % Propositional solver time : 0.000
% 47.79/17.47 % Success case prop preproc time : 0.000
% 47.79/17.47 % Success case prop encoding time : 0.000
% 47.79/17.47 % Success case prop solver time : 0.000
% 47.79/17.47 % Current number of processed clauses : 2722
% 47.79/17.47 % Positive orientable unit clauses : 357
% 47.79/17.47 % Positive unorientable unit clauses: 285
% 47.79/17.47 % Negative unit clauses : 3
% 47.79/17.47 % Non-unit-clauses : 2077
% 47.79/17.47 % Current number of unprocessed clauses: 260302
% 47.79/17.47 % ...number of literals in the above : 588446
% 47.79/17.47 % Current number of archived formulas : 0
% 47.79/17.47 % Current number of archived clauses : 792
% 47.79/17.47 % Clause-clause subsumption calls (NU) : 3321984
% 47.79/17.47 % Rec. Clause-clause subsumption calls : 2327878
% 47.79/17.47 % Non-unit clause-clause subsumptions : 13811
% 47.79/17.47 % Unit Clause-clause subsumption calls : 29740
% 47.79/17.47 % Rewrite failures with RHS unbound : 0
% 47.79/17.47 % BW rewrite match attempts : 5927
% 47.79/17.47 % BW rewrite match successes : 3484
% 47.79/17.47 % Condensation attempts : 0
% 47.79/17.47 % Condensation successes : 0
% 47.79/17.47 % Termbank termtop insertions : 5216418
% 47.79/17.47 % Search garbage collected termcells : 10865
% 47.79/17.47
% 47.79/17.47 % -------------------------------------------------
% 47.79/17.47 % User time : 6.626 s
% 47.79/17.47 % System time : 0.223 s
% 47.79/17.47 % Total time : 6.849 s
% 47.79/17.47 % Maximum resident set size: 9184 pages
% 47.79/17.47
% 47.79/17.47 % -------------------------------------------------
% 47.79/17.47 % User time : 33.050 s
% 47.79/17.47 % System time : 1.022 s
% 47.79/17.47 % Total time : 34.073 s
% 47.79/17.47 % Maximum resident set size: 6912 pages
% 47.79/17.47 % E exiting
%------------------------------------------------------------------------------