%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ITP019+1 : TPTP v8.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n010.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 : Mon Jun 24 09:08:10 EDT 2024 % Result : Theorem 0.58s 0.68s % Output : CNFRefutation 0.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : ITP019+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.11/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Tue Jun 18 22:43:39 EDT 2024 % 0.13/0.35 % CPUTime : % 0.56/0.61 start to proof:theBenchmark % 0.58/0.67 %------------------------------------------- % 0.58/0.67 % File :CSE---1.7 % 0.58/0.67 % Problem :theBenchmark % 0.58/0.67 % Transform :cnf % 0.58/0.67 % Format :tptp:raw % 0.58/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.58/0.67 % 0.58/0.67 % Result :Theorem 0.010000s % 0.58/0.67 % Output :CNFRefutation 0.010000s % 0.58/0.67 %------------------------------------------- % 0.58/0.67 %------------------------------------------------------------------------------ % 0.58/0.67 % File : ITP019+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.58/0.67 % Domain : Interactive Theorem Proving % 0.58/0.67 % Problem : HOL4 syntactic export of thm_2Ecomplex_2ECOMPLEX__INV__NZ.p, bushy mode % 0.58/0.67 % Version : [BG+19] axioms. % 0.58/0.67 % English : % 0.58/0.67 % 0.58/0.67 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall % 0.58/0.67 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe % 0.58/0.67 % Source : [BG+19] % 0.58/0.67 % Names : thm_2Ecomplex_2ECOMPLEX__INV__NZ.p [Gau19] % 0.58/0.67 % : HL409001+1.p [TPAP] % 0.58/0.67 % 0.58/0.67 % Status : Theorem % 0.58/0.67 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.08 v7.5.0 % 0.58/0.67 % Syntax : Number of formulae : 29 ( 10 unt; 0 def) % 0.58/0.68 % Number of atoms : 68 ( 18 equ) % 0.58/0.68 % Maximal formula atoms : 15 ( 2 avg) % 0.58/0.68 % Number of connectives : 45 ( 6 ~; 3 |; 6 &) % 0.58/0.68 % ( 20 <=>; 10 =>; 0 <=; 0 <~>) % 0.58/0.68 % Maximal formula depth : 8 ( 4 avg) % 0.58/0.68 % Maximal term depth : 11 ( 2 avg) % 0.58/0.68 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.58/0.68 % Number of functors : 31 ( 31 usr; 18 con; 0-2 aty) % 0.58/0.68 % Number of variables : 58 ( 57 !; 1 ?) % 0.58/0.68 % SPC : FOF_THM_RFO_SEQ % 0.58/0.68 % 0.58/0.68 % Comments : % 0.58/0.68 % Bugfixes : v7.5.0 - Bugfixes in axioms and export. % 0.58/0.68 %------------------------------------------------------------------------------ % 0.58/0.68 fof(reserved_2Eho_2Eeq__ext,axiom, % 0.58/0.68 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] : % 0.58/0.68 ( ! [V2x_2E0] : s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0),s(A_27a,V2x_2E0))) = s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))) % 0.58/0.68 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Eboolext,axiom, % 0.58/0.68 ! [V0_2E0,V1_2E0] : % 0.58/0.68 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) % 0.58/0.68 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Etruth,axiom, % 0.58/0.68 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Enotfalse,axiom, % 0.58/0.68 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Ebool__cases__ax,axiom, % 0.58/0.68 ! [V0t_2E0] : % 0.58/0.68 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.58/0.68 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Ei__thm,axiom, % 0.58/0.68 ! [A_27a,V0x_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27a),combin_i_2E0),s(A_27a,V0x_2E0))) = s(A_27a,V0x_2E0) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Ek__thm,axiom, % 0.58/0.68 ! [A_27a,A_27b,V0x_2E0,V1y_2E0] : s(A_27a,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27a),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27a)),combin_k_2E0),s(A_27a,V0x_2E0))),s(A_27b,V1y_2E0))) = s(A_27a,V0x_2E0) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Eho_2Es__thm,axiom, % 0.58/0.68 ! [A_27a,A_27b,A_27c,V0f_2E0,V1g_2E0,V2x_2E0] : s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27c),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(A_27a,A_27c))),combin_s_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0))),s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0))),s(A_27a,V2x_2E0))) = s(A_27c,app_2E2(s(tyop_2Emin_2Efun(A_27b,A_27c),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,A_27c)),V0f_2E0),s(A_27a,V2x_2E0))),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0),s(A_27a,V2x_2E0))))) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Elogic_2E_2F_5C,axiom, % 0.58/0.68 ! [V0_2E0,V1_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.58/0.68 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.58/0.68 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Elogic_2E_5C_2F,axiom, % 0.58/0.68 ! [V0_2E0,V1_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.58/0.68 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.58/0.68 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Elogic_2E_7E,axiom, % 0.58/0.68 ! [V0_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) % 0.58/0.68 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Elogic_2E_3D_3D_3E,axiom, % 0.58/0.68 ! [V0_2E0,V1_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_3D_3E_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.58/0.68 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Elogic_2E_3D,axiom, % 0.58/0.68 ! [A_27a,V0_2E0,V1_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0)))) % 0.58/0.68 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Equant_2E_21,axiom, % 0.58/0.68 ! [A_27a,V0f_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.58/0.68 <=> ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(reserved_2Equant_2E_3F,axiom, % 0.58/0.68 ! [A_27a,V0f_2E0] : % 0.58/0.68 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.58/0.68 <=> ? [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0),s(A_27a,V1x_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom, % 0.58/0.68 ! [X0_2E0,X1_2E0] : % 0.58/0.68 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.58/0.68 & p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_2F_5C_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom, % 0.58/0.68 ! [X0_2E0,X1_2E0] : % 0.58/0.68 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.58/0.68 | p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Ebool_2E_5C_2F_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom, % 0.58/0.68 ! [X0_2E0] : % 0.58/0.68 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),c_2Ebool_2E_7E_2E0),s(tyop_2Emin_2Ebool,X0_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom, % 0.58/0.68 ! [X0_2E0,X1_2E0] : % 0.58/0.68 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Efun(tyop_2Emin_2Ebool,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_3D_3E_2E0),s(tyop_2Emin_2Ebool,X0_2E0))),s(tyop_2Emin_2Ebool,X1_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom, % 0.58/0.68 ! [A_27a,X0_2E0,X1_2E0] : % 0.58/0.68 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool)),c_2Emin_2E_3D_2E0),s(A_27a,X0_2E0))),s(A_27a,X1_2E0)))) ) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom, % 0.58/0.68 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_21_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom, % 0.58/0.68 ! [A_27a,X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ebool_2E_3F_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X0_2E0))) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq1_2Ec_2Ecomplex_2Ecomplex__inv_2E1,axiom, % 0.58/0.68 ! [X0_2E0] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__inv_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) ). % 0.58/0.68 % 0.58/0.68 fof(arityeq1_2Ec_2Ecomplex_2Ecomplex__of__num_2E1,axiom, % 0.58/0.68 ! [X0_2E0] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,X0_2E0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),c_2Ecomplex_2Ecomplex__of__num_2E0),s(tyop_2Enum_2Enum,X0_2E0))) ). % 0.58/0.68 % 0.58/0.68 fof(thm_2Ebool_2ETRUTH,axiom, % 0.58/0.68 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.58/0.68 % 0.58/0.68 fof(thm_2Ebool_2EFORALL__SIMP,axiom, % 0.58/0.68 ! [A_27a,V0t_2E0] : % 0.58/0.68 ( ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 0.58/0.68 % 0.58/0.68 fof(thm_2Ebool_2EIMP__CLAUSES,axiom, % 0.58/0.68 ! [V0t_2E0] : % 0.58/0.68 ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.58/0.68 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.58/0.68 & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.58/0.68 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.58/0.68 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.58/0.68 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.58/0.68 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.58/0.68 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 0.58/0.68 % 0.58/0.68 fof(thm_2Ecomplex_2ECOMPLEX__INV__EQ__0,axiom, % 0.58/0.68 ! [V0z_2E0] : % 0.58/0.68 ( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) % 0.58/0.68 <=> s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ) ). % 0.58/0.68 % 0.58/0.68 fof(thm_2Ecomplex_2ECOMPLEX__INV__NZ,conjecture, % 0.58/0.68 ! [V0z_2E0] : % 0.58/0.68 ( s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) % 0.58/0.68 => s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__inv_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),V0z_2E0))) != s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Ecomplex_2Ecomplex__of__num_2E1(s(tyop_2Enum_2Enum,c_2Enum_2E0_2E0))) ) ). % 0.58/0.68 % 0.58/0.68 %------------------------------------------------------------------------------ % 0.58/0.68 %------------------------------------------- % 0.58/0.68 % Proof found % 0.58/0.68 % SZS status Theorem for theBenchmark % 0.58/0.68 % SZS output start Proof % 0.58/0.68 %ClaNum:88(EqnAxiom:33) % 0.58/0.68 %VarNum:241(SingletonVarNum:91) % 0.58/0.68 %MaxLitNum:3 % 0.58/0.68 %MaxfuncDepth:5 % 0.58/0.68 %SharedTerms:44 % 0.58/0.68 %goalClause: 37 46 % 0.58/0.68 %singleGoalClaCount:2 % 0.58/0.68 [36]P1(f5(a1,a2)) % 0.58/0.68 [45]~P1(f5(a1,a4)) % 0.58/0.68 [46]~E(f5(f33(a32,a32),f20(f5(a34,a19))),f5(f33(a32,a32),a6)) % 0.58/0.68 [37]E(f5(f33(a32,a32),f7(f5(f33(a32,a32),a6))),f5(f33(a32,a32),f20(f5(a34,a19)))) % 0.58/0.68 [39]E(f5(f33(a32,a32),f3(f5(f35(a34,f33(a32,a32)),a21),f5(a34,x391))),f5(f33(a32,a32),f20(f5(a34,x391)))) % 0.58/0.68 [42]E(f5(f33(a32,a32),f3(f5(f35(f33(a32,a32),f33(a32,a32)),a14),f5(f33(a32,a32),x421))),f5(f33(a32,a32),f7(f5(f33(a32,a32),x421)))) % 0.58/0.68 [38]E(f5(x381,f3(f5(f35(x381,x381),a26),f5(x381,x382))),f5(x381,x382)) % 0.58/0.68 [40]E(f5(a1,f3(f5(f35(f35(x401,a1),a1),a8),f5(f35(x401,a1),x402))),f5(a1,f9(f5(f35(x401,a1),x402)))) % 0.58/0.68 [41]E(f5(a1,f3(f5(f35(f35(x411,a1),a1),a10),f5(f35(x411,a1),x412))),f5(a1,f13(f5(f35(x411,a1),x412)))) % 0.58/0.68 [43]E(f5(x431,f3(f5(f35(x432,x431),f3(f5(f35(x431,f35(x432,x431)),a27),f5(x431,x433))),f5(x432,x434))),f5(x431,x433)) % 0.58/0.68 [44]E(f5(x441,f3(f5(f35(x442,x441),f3(f5(f35(f35(x442,x443),f35(x442,x441)),f3(f5(f35(f35(x442,f35(x443,x441)),f35(f35(x442,x443),f35(x442,x441))),a28),f5(f35(x442,f35(x443,x441)),x444))),f5(f35(x442,x443),x445))),f5(x442,x446))),f5(x441,f3(f5(f35(x443,x441),f3(f5(f35(x442,f35(x443,x441)),x444),f5(x442,x446))),f5(x443,f3(f5(f35(x442,x443),x445),f5(x442,x446)))))) % 0.58/0.68 [47]E(f5(a1,x471),f5(a1,a2))+E(f5(a1,x471),f5(a1,a4)) % 0.58/0.68 [56]P1(f5(a1,x561))+P1(f5(a1,f15(f5(a1,x561)))) % 0.58/0.68 [57]~P1(f5(a1,x571))+~P1(f5(a1,f15(f5(a1,x571)))) % 0.58/0.68 [67]P1(f5(a1,x671))+P1(f5(a1,f3(f5(f35(a1,a1),a18),f5(a1,x671)))) % 0.58/0.68 [72]~P1(f5(a1,x721))+~P1(f5(a1,f3(f5(f35(a1,a1),a18),f5(a1,x721)))) % 0.58/0.68 [64]~E(f5(f33(a32,a32),x641),f5(f33(a32,a32),f20(f5(a34,a19))))+E(f5(f33(a32,a32),f7(f5(f33(a32,a32),x641))),f5(f33(a32,a32),f20(f5(a34,a19)))) % 0.58/0.68 [71]E(f5(f33(a32,a32),x711),f5(f33(a32,a32),f20(f5(a34,a19))))+~E(f5(f33(a32,a32),f7(f5(f33(a32,a32),x711))),f5(f33(a32,a32),f20(f5(a34,a19)))) % 0.58/0.68 [58]P1(f5(a1,x581))+P1(f5(a1,f22(f5(a1,x581),f5(a1,x582)))) % 0.58/0.68 [59]~P1(f5(a1,x592))+P1(f5(a1,f16(f5(a1,x591),f5(a1,x592)))) % 0.58/0.68 [60]~P1(f5(a1,x601))+P1(f5(a1,f16(f5(a1,x601),f5(a1,x602)))) % 0.58/0.68 [61]~P1(f5(a1,x612))+P1(f5(a1,f22(f5(a1,x611),f5(a1,x612)))) % 0.58/0.68 [65]P1(f5(a1,x651))+~P1(f5(a1,f11(f5(a1,x652),f5(a1,x651)))) % 0.58/0.68 [66]P1(f5(a1,x661))+~P1(f5(a1,f11(f5(a1,x661),f5(a1,x662)))) % 0.58/0.68 [77]P1(f5(a1,x771))+P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a25),f5(a1,x771))),f5(a1,x772)))) % 0.58/0.68 [78]~P1(f5(a1,x782))+P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a17),f5(a1,x781))),f5(a1,x782)))) % 0.58/0.68 [79]~P1(f5(a1,x791))+P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a17),f5(a1,x791))),f5(a1,x792)))) % 0.58/0.68 [80]~P1(f5(a1,x802))+P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a25),f5(a1,x801))),f5(a1,x802)))) % 0.58/0.68 [83]P1(f5(a1,x831))+~P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a12),f5(a1,x832))),f5(a1,x831)))) % 0.58/0.68 [84]P1(f5(a1,x841))+~P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a12),f5(a1,x841))),f5(a1,x842)))) % 0.58/0.68 [75]P1(f5(a1,f3(f5(f35(x751,a1),x752),f5(x751,f29(x751,x752)))))+~P1(f5(a1,f13(f5(f35(x751,a1),x752)))) % 0.58/0.68 [76]~P1(f5(a1,f3(f5(f35(x761,a1),x762),f5(x761,f30(x761,x762)))))+P1(f5(a1,f9(f5(f35(x761,a1),x762)))) % 0.58/0.68 [62]~E(f5(x621,x622),f5(x621,x623))+P1(f5(a1,f23(f5(x621,x622),f5(x621,x623)))) % 0.58/0.68 [69]E(f5(x691,x692),f5(x691,x693))+~P1(f5(a1,f23(f5(x691,x692),f5(x691,x693)))) % 0.58/0.68 [82]~E(f5(x821,x822),f5(x821,x823))+P1(f5(a1,f3(f5(f35(x821,a1),f3(f5(f35(x821,f35(x821,a1)),a24),f5(x821,x822))),f5(x821,x823)))) % 0.58/0.68 [87]E(f5(x871,x872),f5(x871,x873))+~P1(f5(a1,f3(f5(f35(x871,a1),f3(f5(f35(x871,f35(x871,a1)),a24),f5(x871,x872))),f5(x871,x873)))) % 0.58/0.68 [73]P1(f5(a1,f3(f5(f35(x731,a1),x732),f5(x731,x733))))+~P1(f5(a1,f9(f5(f35(x731,a1),x732)))) % 0.58/0.68 [74]~P1(f5(a1,f3(f5(f35(x741,a1),x742),f5(x741,x743))))+P1(f5(a1,f13(f5(f35(x741,a1),x742)))) % 0.58/0.68 [88]E(f5(f35(x881,x882),x883),f5(f35(x881,x882),x884))+~E(f5(x882,f3(f5(f35(x881,x882),x883),f5(x881,f31(x881,x882,x883,x884)))),f5(x882,f3(f5(f35(x881,x882),x884),f5(x881,f31(x881,x882,x883,x884))))) % 0.58/0.68 [52]E(f5(a1,x521),f5(a1,x522))+P1(f5(a1,x521))+P1(f5(a1,x522)) % 0.58/0.68 [55]E(f5(a1,x551),f5(a1,x552))+~P1(f5(a1,x551))+~P1(f5(a1,x552)) % 0.58/0.68 [63]~P1(f5(a1,x631))+~P1(f5(a1,x632))+P1(f5(a1,f11(f5(a1,x631),f5(a1,x632)))) % 0.58/0.68 [68]P1(f5(a1,x681))+P1(f5(a1,x682))+~P1(f5(a1,f16(f5(a1,x682),f5(a1,x681)))) % 0.58/0.68 [70]P1(f5(a1,x701))+~P1(f5(a1,x702))+~P1(f5(a1,f22(f5(a1,x702),f5(a1,x701)))) % 0.58/0.69 [81]~P1(f5(a1,x811))+~P1(f5(a1,x812))+P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a12),f5(a1,x811))),f5(a1,x812)))) % 0.58/0.69 [85]P1(f5(a1,x851))+P1(f5(a1,x852))+~P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a17),f5(a1,x852))),f5(a1,x851)))) % 0.58/0.69 [86]P1(f5(a1,x861))+~P1(f5(a1,x862))+~P1(f5(a1,f3(f5(f35(a1,a1),f3(f5(f35(a1,f35(a1,a1)),a25),f5(a1,x862))),f5(a1,x861)))) % 0.58/0.69 %EqnAxiom % 0.58/0.69 [1]E(x11,x11) % 0.58/0.69 [2]E(x22,x21)+~E(x21,x22) % 0.58/0.69 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.58/0.69 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 0.58/0.69 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 0.58/0.69 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 0.58/0.69 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 0.58/0.69 [8]~E(x81,x82)+E(f31(x81,x83,x84,x85),f31(x82,x83,x84,x85)) % 0.58/0.69 [9]~E(x91,x92)+E(f31(x93,x91,x94,x95),f31(x93,x92,x94,x95)) % 0.58/0.69 [10]~E(x101,x102)+E(f31(x103,x104,x101,x105),f31(x103,x104,x102,x105)) % 0.58/0.69 [11]~E(x111,x112)+E(f31(x113,x114,x115,x111),f31(x113,x114,x115,x112)) % 0.58/0.69 [12]~E(x121,x122)+E(f33(x121,x123),f33(x122,x123)) % 0.58/0.69 [13]~E(x131,x132)+E(f33(x133,x131),f33(x133,x132)) % 0.58/0.69 [14]~E(x141,x142)+E(f35(x141,x143),f35(x142,x143)) % 0.58/0.69 [15]~E(x151,x152)+E(f35(x153,x151),f35(x153,x152)) % 0.58/0.69 [16]~E(x161,x162)+E(f15(x161),f15(x162)) % 0.58/0.69 [17]~E(x171,x172)+E(f7(x171),f7(x172)) % 0.58/0.69 [18]~E(x181,x182)+E(f11(x181,x183),f11(x182,x183)) % 0.58/0.69 [19]~E(x191,x192)+E(f11(x193,x191),f11(x193,x192)) % 0.58/0.69 [20]~E(x201,x202)+E(f20(x201),f20(x202)) % 0.58/0.69 [21]~E(x211,x212)+E(f29(x211,x213),f29(x212,x213)) % 0.58/0.69 [22]~E(x221,x222)+E(f29(x223,x221),f29(x223,x222)) % 0.58/0.69 [23]~E(x231,x232)+E(f13(x231),f13(x232)) % 0.58/0.69 [24]~E(x241,x242)+E(f9(x241),f9(x242)) % 0.58/0.69 [25]~E(x251,x252)+E(f22(x251,x253),f22(x252,x253)) % 0.58/0.69 [26]~E(x261,x262)+E(f22(x263,x261),f22(x263,x262)) % 0.58/0.69 [27]~E(x271,x272)+E(f16(x271,x273),f16(x272,x273)) % 0.58/0.69 [28]~E(x281,x282)+E(f16(x283,x281),f16(x283,x282)) % 0.58/0.69 [29]~E(x291,x292)+E(f23(x291,x293),f23(x292,x293)) % 0.58/0.69 [30]~E(x301,x302)+E(f23(x303,x301),f23(x303,x302)) % 0.58/0.69 [31]~E(x311,x312)+E(f30(x311,x313),f30(x312,x313)) % 0.58/0.69 [32]~E(x321,x322)+E(f30(x323,x321),f30(x323,x322)) % 0.58/0.69 [33]~P1(x331)+P1(x332)+~E(x331,x332) % 0.58/0.69 % 0.58/0.69 %------------------------------------------- % 0.58/0.69 cnf(93,plain, % 0.58/0.69 (E(f5(f33(a32,a32),a6),f5(f33(a32,a32),f20(f5(a34,a19))))), % 0.58/0.69 inference(scs_inference,[],[37,71])). % 0.58/0.69 cnf(108,plain, % 0.58/0.69 ($false), % 0.58/0.69 inference(scs_inference,[],[46,93,2]), % 0.58/0.69 ['proof']). % 0.58/0.69 % SZS output end Proof % 0.58/0.69 % Total time :0.010000s %------------------------------------------------------------------------------