%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ITP023+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 : n026.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:17 EDT 2024 % Result : Theorem 0.52s 0.65s % Output : CNFRefutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ITP023+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n026.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Tue Jun 18 21:47:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.57 start to proof:theBenchmark % 0.52/0.63 %------------------------------------------- % 0.52/0.63 % File :CSE---1.7 % 0.52/0.64 % Problem :theBenchmark % 0.52/0.64 % Transform :cnf % 0.52/0.64 % Format :tptp:raw % 0.52/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.52/0.64 % 0.52/0.64 % Result :Theorem 0.000000s % 0.52/0.64 % Output :CNFRefutation 0.000000s % 0.52/0.64 %------------------------------------------- % 0.52/0.64 %------------------------------------------------------------------------------ % 0.52/0.64 % File : ITP023+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.52/0.64 % Domain : Interactive Theorem Proving % 0.52/0.64 % Problem : HOL4 syntactic export of thm_2Ereal__topology_2EBOUNDED__BALL.p, bushy mode % 0.52/0.64 % Version : [BG+19] axioms. % 0.52/0.64 % English : % 0.52/0.64 % 0.52/0.64 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall % 0.52/0.64 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe % 0.52/0.64 % Source : [BG+19] % 0.52/0.64 % Names : thm_2Ereal__topology_2EBOUNDED__BALL.p [Gau19] % 0.52/0.64 % : HL411001+1.p [TPAP] % 0.52/0.64 % 0.52/0.64 % Status : Theorem % 0.52/0.64 % Rating : 0.33 v8.2.0, 0.36 v7.5.0 % 0.52/0.64 % Syntax : Number of formulae : 53 ( 16 unt; 0 def) % 0.52/0.64 % Number of atoms : 191 ( 25 equ) % 0.52/0.64 % Maximal formula atoms : 15 ( 3 avg) % 0.52/0.64 % Number of connectives : 186 ( 48 ~; 36 |; 26 &) % 0.52/0.64 % ( 44 <=>; 32 =>; 0 <=; 0 <~>) % 0.52/0.64 % Maximal formula depth : 11 ( 5 avg) % 0.52/0.64 % Maximal term depth : 11 ( 2 avg) % 0.52/0.64 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.52/0.64 % Number of functors : 35 ( 35 usr; 19 con; 0-2 aty) % 0.52/0.64 % Number of variables : 107 ( 105 !; 2 ?) % 0.52/0.64 % SPC : FOF_THM_RFO_SEQ % 0.52/0.64 % 0.52/0.64 % Comments : % 0.52/0.64 % Bugfixes : v7.5.0 - Bugfixes in axioms and export. % 0.52/0.64 %------------------------------------------------------------------------------ % 0.52/0.64 fof(reserved_2Eho_2Eeq__ext,axiom, % 0.52/0.64 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] : % 0.52/0.64 ( ! [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.52/0.64 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Eboolext,axiom, % 0.52/0.64 ! [V0_2E0,V1_2E0] : % 0.52/0.64 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.52/0.64 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) % 0.52/0.64 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Etruth,axiom, % 0.52/0.64 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Enotfalse,axiom, % 0.52/0.64 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Ebool__cases__ax,axiom, % 0.52/0.64 ! [V0t_2E0] : % 0.52/0.64 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.52/0.64 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Ei__thm,axiom, % 0.52/0.64 ! [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.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Ek__thm,axiom, % 0.52/0.64 ! [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.52/0.64 % 0.52/0.64 fof(reserved_2Eho_2Es__thm,axiom, % 0.52/0.64 ! [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.52/0.64 % 0.52/0.64 fof(reserved_2Elogic_2E_2F_5C,axiom, % 0.52/0.64 ! [V0_2E0,V1_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.52/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.52/0.64 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Elogic_2E_5C_2F,axiom, % 0.52/0.64 ! [V0_2E0,V1_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.52/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.52/0.64 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Elogic_2E_7E,axiom, % 0.52/0.64 ! [V0_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) % 0.52/0.64 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Elogic_2E_3D_3D_3E,axiom, % 0.52/0.64 ! [V0_2E0,V1_2E0] : % 0.52/0.64 ( 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.52/0.64 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.52/0.64 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Elogic_2E_3D,axiom, % 0.52/0.64 ! [A_27a,V0_2E0,V1_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0)))) % 0.52/0.64 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ). % 0.52/0.64 % 0.52/0.64 fof(reserved_2Equant_2E_21,axiom, % 0.52/0.64 ! [A_27a,V0f_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.52/0.64 <=> ! [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.52/0.64 % 0.52/0.64 fof(reserved_2Equant_2E_3F,axiom, % 0.52/0.64 ! [A_27a,V0f_2E0] : % 0.52/0.64 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.52/0.64 <=> ? [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.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom, % 0.52/0.64 ! [X0_2E0,X1_2E0] : % 0.52/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.52/0.64 & p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.52/0.64 <=> 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.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom, % 0.52/0.64 ! [X0_2E0,X1_2E0] : % 0.52/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.52/0.64 | p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.52/0.64 <=> 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.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom, % 0.52/0.64 ! [X0_2E0] : % 0.52/0.64 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.52/0.64 <=> 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.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom, % 0.52/0.64 ! [X0_2E0,X1_2E0] : % 0.52/0.64 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.52/0.64 => p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.52/0.64 <=> 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.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom, % 0.52/0.64 ! [A_27a,X0_2E0,X1_2E0] : % 0.52/0.64 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0) % 0.52/0.64 <=> 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.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom, % 0.52/0.64 ! [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.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom, % 0.52/0.64 ! [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.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ereal__topology_2Ebounded__def_2E1,axiom, % 0.52/0.64 ! [X0_2E0] : s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X0_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),c_2Ereal__topology_2Ebounded__def_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X0_2E0))) ). % 0.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Epair_2E_2C_2E2_2Emono_2Etyop_2Erealax_2Ereal_20mono_2Etyop_2Erealax_2Ereal,axiom, % 0.52/0.64 ! [X0_2E0,X1_2E0] : s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,X0_2E0),s(tyop_2Erealax_2Ereal,X1_2E0))) = s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal))),c_2Epair_2E_2C_2E0),s(tyop_2Erealax_2Ereal,X0_2E0))),s(tyop_2Erealax_2Ereal,X1_2E0))) ). % 0.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ereal__topology_2Eball_2E1,axiom, % 0.52/0.64 ! [X0_2E0] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Eball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) ). % 0.52/0.64 % 0.52/0.64 fof(arityeq1_2Ec_2Ereal__topology_2Ecball_2E1,axiom, % 0.52/0.64 ! [X0_2E0] : s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) = s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool)),c_2Ereal__topology_2Ecball_2E0),s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),X0_2E0))) ). % 0.52/0.64 % 0.52/0.64 fof(arityeq2_2Ec_2Epred__set_2ESUBSET_2E2_2Emono_2Etyop_2Erealax_2Ereal,axiom, % 0.52/0.64 ! [X0_2E0,X1_2E0] : s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),c_2Epred__set_2ESUBSET_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),X1_2E0))) ). % 0.52/0.64 % 0.52/0.64 fof(thm_2Ebool_2ETRUTH,axiom, % 0.52/0.64 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.52/0.64 % 0.52/0.64 fof(thm_2Ebool_2EIMP__ANTISYM__AX,axiom, % 0.52/0.64 ! [V0t1_2E0,V1t2_2E0] : % 0.52/0.64 ( ( p(s(tyop_2Emin_2Ebool,V0t1_2E0)) % 0.52/0.64 => p(s(tyop_2Emin_2Ebool,V1t2_2E0)) ) % 0.52/0.64 => ( ( p(s(tyop_2Emin_2Ebool,V1t2_2E0)) % 0.52/0.64 => p(s(tyop_2Emin_2Ebool,V0t1_2E0)) ) % 0.52/0.65 => s(tyop_2Emin_2Ebool,V0t1_2E0) = s(tyop_2Emin_2Ebool,V1t2_2E0) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EIMP__F,axiom, % 0.52/0.65 ! [V0t_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 => ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EF__IMP,axiom, % 0.52/0.65 ! [V0t_2E0] : % 0.52/0.65 ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EIMP__CLAUSES,axiom, % 0.52/0.65 ! [V0t_2E0] : % 0.52/0.65 ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.52/0.65 & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.52/0.65 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.52/0.65 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2ENOT__CLAUSES,axiom, % 0.52/0.65 ( ! [V0t_2E0] : % 0.52/0.65 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EEQ__SYM__EQ,axiom, % 0.52/0.65 ! [A_27a,V0x_2E0,V1y_2E0] : % 0.52/0.65 ( s(A_27a,V0x_2E0) = s(A_27a,V1y_2E0) % 0.52/0.65 <=> s(A_27a,V1y_2E0) = s(A_27a,V0x_2E0) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EEQ__CLAUSES,axiom, % 0.52/0.65 ! [V0t_2E0] : % 0.52/0.65 ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 0.52/0.65 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.52/0.65 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) % 0.52/0.65 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2ENOT__FORALL__THM,axiom, % 0.52/0.65 ! [A_27a,V0P_2E0] : % 0.52/0.65 ( ~ ! [V1x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V1x_2E0)))) % 0.52/0.65 <=> ? [V2x_2E0] : ~ p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V2x_2E0)))) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EDISJ__ASSOC,axiom, % 0.52/0.65 ! [V0A_2E0,V1B_2E0,V2C_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1B_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V2C_2E0)) ) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1B_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V2C_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EDISJ__SYM,axiom, % 0.52/0.65 ! [V0A_2E0,V1B_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V1B_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0A_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ebool_2EDE__MORGAN__THM,axiom, % 0.52/0.65 ! [V0A_2E0,V1B_2E0] : % 0.52/0.65 ( ( ~ ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 & p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) % 0.52/0.65 <=> ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) ) % 0.52/0.65 & ( ~ ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) % 0.52/0.65 <=> ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 & ~ p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ereal__topology_2EBALL__SUBSET__CBALL,axiom, % 0.52/0.65 ! [V0x_2E0,V1e_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,V0x_2E0),s(tyop_2Erealax_2Ereal,V1e_2E0))))),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,V0x_2E0),s(tyop_2Erealax_2Ereal,V1e_2E0)))))))) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ereal__topology_2EBOUNDED__SUBSET,axiom, % 0.52/0.65 ! [V0s_2E0,V1t_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),V1t_2E0)))) % 0.52/0.65 & p(s(tyop_2Emin_2Ebool,c_2Epred__set_2ESUBSET_2E2(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),V1t_2E0)))) ) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),V0s_2E0)))) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ereal__topology_2EBOUNDED__CBALL,axiom, % 0.52/0.65 ! [V0x_2E0,V1e_2E0] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Ecball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,V0x_2E0),s(tyop_2Erealax_2Ereal,V1e_2E0)))))))) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2ENOT__NOT,axiom, % 0.52/0.65 ! [V0t_2E0] : % 0.52/0.65 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.52/0.65 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2EAND__INV__IMP,axiom, % 0.52/0.65 ! [V0A_2E0] : % 0.52/0.65 ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 => ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2EOR__DUAL2,axiom, % 0.52/0.65 ! [V0B_2E0,V1A_2E0] : % 0.52/0.65 ( ( ~ ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2EOR__DUAL3,axiom, % 0.52/0.65 ! [V0B_2E0,V1A_2E0] : % 0.52/0.65 ( ( ~ ( ~ p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.52/0.65 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2EAND__INV2,axiom, % 0.52/0.65 ! [V0A_2E0] : % 0.52/0.65 ( ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 => ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2Edc__eq,axiom, % 0.52/0.65 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 <=> s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2Edc__conj,axiom, % 0.52/0.65 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 & p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2Edc__disj,axiom, % 0.52/0.65 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2Edc__imp,axiom, % 0.52/0.65 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 => p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.52/0.65 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.52/0.65 & ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Esat_2Edc__neg,axiom, % 0.52/0.65 ! [V0q_2E0,V1p_2E0] : % 0.52/0.65 ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 0.52/0.65 <=> ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 0.52/0.65 <=> ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 0.52/0.65 | p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 0.52/0.65 & ( ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) % 0.52/0.65 | ~ p(s(tyop_2Emin_2Ebool,V1p_2E0)) ) ) ) ). % 0.52/0.65 % 0.52/0.65 fof(thm_2Ereal__topology_2EBOUNDED__BALL,conjecture, % 0.52/0.65 ! [V0x_2E0,V1e_2E0] : p(s(tyop_2Emin_2Ebool,c_2Ereal__topology_2Ebounded__def_2E1(s(tyop_2Emin_2Efun(tyop_2Erealax_2Ereal,tyop_2Emin_2Ebool),c_2Ereal__topology_2Eball_2E1(s(tyop_2Epair_2Eprod(tyop_2Erealax_2Ereal,tyop_2Erealax_2Ereal),c_2Epair_2E_2C_2E2(s(tyop_2Erealax_2Ereal,V0x_2E0),s(tyop_2Erealax_2Ereal,V1e_2E0)))))))) ). % 0.52/0.65 % 0.52/0.65 %------------------------------------------------------------------------------ % 0.52/0.65 %------------------------------------------- % 0.52/0.65 % Proof found % 0.52/0.65 % SZS status Theorem for theBenchmark % 0.52/0.65 % SZS output start Proof % 0.52/0.65 %ClaNum:142(EqnAxiom:45) % 0.52/0.65 %VarNum:362(SingletonVarNum:150) % 0.52/0.65 %MaxLitNum:4 % 0.52/0.65 %MaxfuncDepth:7 % 0.52/0.65 %SharedTerms:54 % 0.52/0.65 %goalClause: 62 % 0.52/0.65 %singleGoalClaCount:1 % 0.52/0.65 [48]P1(f5(a1,a2)) % 0.52/0.65 [61]~P1(f5(a1,a4)) % 0.52/0.65 [62]~P1(f5(a1,f28(f5(f40(a41,a1),f27(f5(f42(a41,a41),f24(f5(a41,a33),f5(a41,a39)))))))) % 0.52/0.65 [50]E(f5(a1,f3(f5(f40(f40(a41,a1),a1),a7),f5(f40(a41,a1),x501))),f5(a1,f28(f5(f40(a41,a1),x501)))) % 0.52/0.65 [53]E(f5(f40(a41,a1),f3(f5(f40(f42(a41,a41),f40(a41,a1)),a14),f5(f42(a41,a41),x531))),f5(f40(a41,a1),f27(f5(f42(a41,a41),x531)))) % 0.52/0.65 [54]E(f5(f40(a41,a1),f3(f5(f40(f42(a41,a41),f40(a41,a1)),a29),f5(f42(a41,a41),x541))),f5(f40(a41,a1),f30(f5(f42(a41,a41),x541)))) % 0.52/0.65 [49]E(f5(x491,f3(f5(f40(x491,x491),a6),f5(x491,x492))),f5(x491,x492)) % 0.52/0.65 [56]E(f5(f42(a41,a41),f3(f5(f40(a41,f42(a41,a41)),f3(f5(f40(a41,f40(a41,f42(a41,a41))),a15),f5(a41,x561))),f5(a41,x562))),f5(f42(a41,a41),f24(f5(a41,x561),f5(a41,x562)))) % 0.52/0.65 [51]E(f5(a1,f3(f5(f40(f40(x511,a1),a1),a8),f5(f40(x511,a1),x512))),f5(a1,f9(f5(f40(x511,a1),x512)))) % 0.52/0.65 [52]E(f5(a1,f3(f5(f40(f40(x521,a1),a1),a10),f5(f40(x521,a1),x522))),f5(a1,f13(f5(f40(x521,a1),x522)))) % 0.52/0.65 [57]E(f5(a1,f3(f5(f40(f40(a41,a1),a1),f3(f5(f40(f40(a41,a1),f40(f40(a41,a1),a1)),a25),f5(f40(a41,a1),x571))),f5(f40(a41,a1),x572))),f5(a1,f26(f5(f40(a41,a1),x571),f5(f40(a41,a1),x572)))) % 0.52/0.65 [58]P1(f5(a1,f28(f5(f40(a41,a1),f30(f5(f42(a41,a41),f24(f5(a41,x581),f5(a41,x582)))))))) % 0.52/0.65 [59]P1(f5(a1,f26(f5(f40(a41,a1),f27(f5(f42(a41,a41),f24(f5(a41,x591),f5(a41,x592))))),f5(f40(a41,a1),f30(f5(f42(a41,a41),f24(f5(a41,x591),f5(a41,x592)))))))) % 0.52/0.65 [55]E(f5(x551,f3(f5(f40(x552,x551),f3(f5(f40(x551,f40(x552,x551)),a31),f5(x551,x553))),f5(x552,x554))),f5(x551,x553)) % 0.52/0.65 [60]E(f5(x601,f3(f5(f40(x602,x601),f3(f5(f40(f40(x602,x603),f40(x602,x601)),f3(f5(f40(f40(x602,f40(x603,x601)),f40(f40(x602,x603),f40(x602,x601))),a32),f5(f40(x602,f40(x603,x601)),x604))),f5(f40(x602,x603),x605))),f5(x602,x606))),f5(x601,f3(f5(f40(x603,x601),f3(f5(f40(x602,f40(x603,x601)),x604),f5(x602,x606))),f5(x603,f3(f5(f40(x602,x603),x605),f5(x602,x606)))))) % 0.52/0.65 [63]E(f5(a1,x631),f5(a1,a2))+E(f5(a1,x631),f5(a1,a4)) % 0.52/0.65 [67]E(f5(a1,x671),f5(a1,a4))+P1(f5(a1,x671)) % 0.52/0.65 [68]E(f5(a1,a4),f5(a1,x681))+P1(f5(a1,x681)) % 0.52/0.65 [71]~E(f5(a1,x711),f5(a1,a2))+P1(f5(a1,x711)) % 0.52/0.65 [72]~E(f5(a1,a2),f5(a1,x721))+P1(f5(a1,x721)) % 0.52/0.65 [73]E(f5(a1,x731),f5(a1,a2))+~P1(f5(a1,x731)) % 0.52/0.65 [74]E(f5(a1,a2),f5(a1,x741))+~P1(f5(a1,x741)) % 0.52/0.65 [80]~E(f5(a1,x801),f5(a1,a4))+~P1(f5(a1,x801)) % 0.52/0.65 [81]~E(f5(a1,a4),f5(a1,x811))+~P1(f5(a1,x811)) % 0.52/0.65 [99]P1(f5(a1,x991))+P1(f5(a1,f16(f5(a1,x991)))) % 0.52/0.65 [110]~P1(f5(a1,x1101))+~P1(f5(a1,f16(f5(a1,x1101)))) % 0.52/0.65 [119]P1(f5(a1,x1191))+P1(f5(a1,f3(f5(f40(a1,a1),a19),f5(a1,x1191)))) % 0.52/0.65 [123]~P1(f5(a1,x1231))+~P1(f5(a1,f3(f5(f40(a1,a1),a19),f5(a1,x1231)))) % 0.52/0.65 [111]P1(f5(a1,x1111))+P1(f5(a1,f20(f5(a1,x1111),f5(a1,x1112)))) % 0.52/0.65 [112]~P1(f5(a1,x1122))+P1(f5(a1,f17(f5(a1,x1121),f5(a1,x1122)))) % 0.52/0.65 [113]~P1(f5(a1,x1131))+P1(f5(a1,f17(f5(a1,x1131),f5(a1,x1132)))) % 0.52/0.65 [114]~P1(f5(a1,x1142))+P1(f5(a1,f20(f5(a1,x1141),f5(a1,x1142)))) % 0.52/0.65 [117]P1(f5(a1,x1171))+~P1(f5(a1,f11(f5(a1,x1172),f5(a1,x1171)))) % 0.52/0.65 [118]P1(f5(a1,x1181))+~P1(f5(a1,f11(f5(a1,x1181),f5(a1,x1182)))) % 0.52/0.65 [131]P1(f5(a1,x1311))+P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a23),f5(a1,x1311))),f5(a1,x1312)))) % 0.52/0.65 [132]~P1(f5(a1,x1322))+P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a18),f5(a1,x1321))),f5(a1,x1322)))) % 0.52/0.65 [133]~P1(f5(a1,x1331))+P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a18),f5(a1,x1331))),f5(a1,x1332)))) % 0.52/0.65 [134]~P1(f5(a1,x1342))+P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a23),f5(a1,x1341))),f5(a1,x1342)))) % 0.52/0.65 [137]P1(f5(a1,x1371))+~P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a12),f5(a1,x1372))),f5(a1,x1371)))) % 0.52/0.65 [138]P1(f5(a1,x1381))+~P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a12),f5(a1,x1381))),f5(a1,x1382)))) % 0.52/0.65 [126]P1(f5(a1,f3(f5(f40(x1261,a1),x1262),f5(x1261,f34(x1261,x1262)))))+~P1(f5(a1,f13(f5(f40(x1261,a1),x1262)))) % 0.52/0.65 [127]~P1(f5(a1,f3(f5(f40(x1271,a1),x1272),f5(x1271,f35(x1271,x1272)))))+P1(f5(a1,f9(f5(f40(x1271,a1),x1272)))) % 0.52/0.65 [115]~E(f5(x1151,x1152),f5(x1151,x1153))+P1(f5(a1,f21(f5(x1151,x1152),f5(x1151,x1153)))) % 0.52/0.65 [121]E(f5(x1211,x1212),f5(x1211,x1213))+~P1(f5(a1,f21(f5(x1211,x1212),f5(x1211,x1213)))) % 0.52/0.65 [136]~E(f5(x1361,x1362),f5(x1361,x1363))+P1(f5(a1,f3(f5(f40(x1361,a1),f3(f5(f40(x1361,f40(x1361,a1)),a22),f5(x1361,x1362))),f5(x1361,x1363)))) % 0.52/0.65 [141]E(f5(x1411,x1412),f5(x1411,x1413))+~P1(f5(a1,f3(f5(f40(x1411,a1),f3(f5(f40(x1411,f40(x1411,a1)),a22),f5(x1411,x1412))),f5(x1411,x1413)))) % 0.52/0.65 [124]P1(f5(a1,f3(f5(f40(x1241,a1),x1242),f5(x1241,x1243))))+~P1(f5(a1,f9(f5(f40(x1241,a1),x1242)))) % 0.52/0.65 [125]~P1(f5(a1,f3(f5(f40(x1251,a1),x1252),f5(x1251,x1253))))+P1(f5(a1,f13(f5(f40(x1251,a1),x1252)))) % 0.52/0.65 [128]P1(f5(a1,f3(f5(f40(x1281,a1),x1282),f5(x1281,x1283))))+~P1(f5(a1,f3(f5(f40(x1281,a1),x1282),f5(x1281,f37(x1281,x1282))))) % 0.52/0.65 [129]P1(f5(a1,f3(f5(f40(x1291,a1),x1292),f5(x1291,x1293))))+~P1(f5(a1,f3(f5(f40(x1291,a1),x1292),f5(x1291,f38(x1291,x1292))))) % 0.52/0.65 [142]E(f5(f40(x1421,x1422),x1423),f5(f40(x1421,x1422),x1424))+~E(f5(x1422,f3(f5(f40(x1421,x1422),x1423),f5(x1421,f36(x1421,x1422,x1423,x1424)))),f5(x1422,f3(f5(f40(x1421,x1422),x1424),f5(x1421,f36(x1421,x1422,x1423,x1424))))) % 0.52/0.65 [79]E(f5(a1,x791),f5(a1,x792))+P1(f5(a1,x791))+P1(f5(a1,x792)) % 0.52/0.65 [87]E(f5(a1,x871),f5(a1,x872))+~P1(f5(a1,x871))+~P1(f5(a1,x872)) % 0.52/0.65 [116]~P1(f5(a1,x1161))+~P1(f5(a1,x1162))+P1(f5(a1,f11(f5(a1,x1161),f5(a1,x1162)))) % 0.52/0.65 [120]P1(f5(a1,x1201))+P1(f5(a1,x1202))+~P1(f5(a1,f17(f5(a1,x1202),f5(a1,x1201)))) % 0.52/0.65 [122]P1(f5(a1,x1221))+~P1(f5(a1,x1222))+~P1(f5(a1,f20(f5(a1,x1222),f5(a1,x1221)))) % 0.52/0.65 [135]~P1(f5(a1,x1351))+~P1(f5(a1,x1352))+P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a12),f5(a1,x1351))),f5(a1,x1352)))) % 0.52/0.65 [139]P1(f5(a1,x1391))+P1(f5(a1,x1392))+~P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a18),f5(a1,x1392))),f5(a1,x1391)))) % 0.52/0.65 [140]P1(f5(a1,x1401))+~P1(f5(a1,x1402))+~P1(f5(a1,f3(f5(f40(a1,a1),f3(f5(f40(a1,f40(a1,a1)),a23),f5(a1,x1402))),f5(a1,x1401)))) % 0.52/0.65 [130]P1(f5(a1,f28(f5(f40(a41,a1),x1301))))+~P1(f5(a1,f26(f5(f40(a41,a1),x1301),f5(f40(a41,a1),x1302))))+~P1(f5(a1,f28(f5(f40(a41,a1),x1302)))) % 0.52/0.65 [85]P2(x853,x851,x852)+E(f5(a1,x851),f5(a1,x852))+P1(f5(a1,x853)) % 0.52/0.65 [89]P2(x891,x892,x893)+P1(f5(a1,x893))+~P1(f5(a1,x892)) % 0.52/0.65 [91]P2(x911,x912,x913)+P1(f5(a1,x913))+~P1(f5(a1,x911)) % 0.52/0.65 [92]P2(x921,x922,x923)+~E(f5(a1,x922),f5(a1,x923))+~P1(f5(a1,x921)) % 0.52/0.65 [94]P2(x941,x942,x943)+~P1(f5(a1,x941))+~P1(f5(a1,x942)) % 0.52/0.65 [98]~P2(x981,x982,x983)+~E(f5(a1,x982),f5(a1,x983))+P1(f5(a1,x981)) % 0.52/0.65 [97]P2(x971,x972,x973)+P1(f5(a1,x972))+P1(f5(a1,x971))+~P1(f5(a1,x973)) % 0.52/0.65 [100]~P2(x1003,x1002,x1001)+P1(f5(a1,x1001))+P1(f5(a1,x1002))+P1(f5(a1,x1003)) % 0.52/0.65 [104]~P2(x1043,x1041,x1042)+E(f5(a1,x1041),f5(a1,x1042))+P1(f5(a1,x1041))+~P1(f5(a1,x1043)) % 0.52/0.65 [107]~P2(x1073,x1071,x1072)+E(f5(a1,x1071),f5(a1,x1072))+~P1(f5(a1,x1072))+~P1(f5(a1,x1073)) % 0.52/0.65 [108]~P2(x1082,x1081,x1083)+~P1(f5(a1,x1082))+~P1(f5(a1,x1083))+P1(f5(a1,x1081)) % 0.52/0.65 [109]~P2(x1091,x1092,x1093)+~P1(f5(a1,x1092))+~P1(f5(a1,x1093))+P1(f5(a1,x1091)) % 0.52/0.65 %EqnAxiom % 0.52/0.65 [1]E(x11,x11) % 0.52/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.52/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.52/0.65 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 0.52/0.65 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 0.52/0.65 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 0.52/0.65 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 0.52/0.65 [8]~E(x81,x82)+E(f36(x81,x83,x84,x85),f36(x82,x83,x84,x85)) % 0.52/0.65 [9]~E(x91,x92)+E(f36(x93,x91,x94,x95),f36(x93,x92,x94,x95)) % 0.52/0.65 [10]~E(x101,x102)+E(f36(x103,x104,x101,x105),f36(x103,x104,x102,x105)) % 0.52/0.65 [11]~E(x111,x112)+E(f36(x113,x114,x115,x111),f36(x113,x114,x115,x112)) % 0.52/0.65 [12]~E(x121,x122)+E(f40(x121,x123),f40(x122,x123)) % 0.52/0.65 [13]~E(x131,x132)+E(f40(x133,x131),f40(x133,x132)) % 0.52/0.65 [14]~E(x141,x142)+E(f38(x141,x143),f38(x142,x143)) % 0.52/0.66 [15]~E(x151,x152)+E(f38(x153,x151),f38(x153,x152)) % 0.52/0.66 [16]~E(x161,x162)+E(f16(x161),f16(x162)) % 0.52/0.66 [17]~E(x171,x172)+E(f42(x171,x173),f42(x172,x173)) % 0.52/0.66 [18]~E(x181,x182)+E(f42(x183,x181),f42(x183,x182)) % 0.52/0.66 [19]~E(x191,x192)+E(f37(x191,x193),f37(x192,x193)) % 0.52/0.66 [20]~E(x201,x202)+E(f37(x203,x201),f37(x203,x202)) % 0.52/0.66 [21]~E(x211,x212)+E(f28(x211),f28(x212)) % 0.52/0.66 [22]~E(x221,x222)+E(f17(x221,x223),f17(x222,x223)) % 0.52/0.66 [23]~E(x231,x232)+E(f17(x233,x231),f17(x233,x232)) % 0.52/0.66 [24]~E(x241,x242)+E(f26(x241,x243),f26(x242,x243)) % 0.52/0.66 [25]~E(x251,x252)+E(f26(x253,x251),f26(x253,x252)) % 0.52/0.66 [26]~E(x261,x262)+E(f30(x261),f30(x262)) % 0.52/0.66 [27]~E(x271,x272)+E(f24(x271,x273),f24(x272,x273)) % 0.52/0.66 [28]~E(x281,x282)+E(f24(x283,x281),f24(x283,x282)) % 0.52/0.66 [29]~E(x291,x292)+E(f13(x291),f13(x292)) % 0.52/0.66 [30]~E(x301,x302)+E(f20(x301,x303),f20(x302,x303)) % 0.52/0.66 [31]~E(x311,x312)+E(f20(x313,x311),f20(x313,x312)) % 0.52/0.66 [32]~E(x321,x322)+E(f9(x321),f9(x322)) % 0.52/0.66 [33]~E(x331,x332)+E(f11(x331,x333),f11(x332,x333)) % 0.52/0.66 [34]~E(x341,x342)+E(f11(x343,x341),f11(x343,x342)) % 0.52/0.66 [35]~E(x351,x352)+E(f27(x351),f27(x352)) % 0.52/0.66 [36]~E(x361,x362)+E(f34(x361,x363),f34(x362,x363)) % 0.52/0.66 [37]~E(x371,x372)+E(f34(x373,x371),f34(x373,x372)) % 0.52/0.66 [38]~E(x381,x382)+E(f21(x381,x383),f21(x382,x383)) % 0.52/0.66 [39]~E(x391,x392)+E(f21(x393,x391),f21(x393,x392)) % 0.52/0.66 [40]~E(x401,x402)+E(f35(x401,x403),f35(x402,x403)) % 0.52/0.66 [41]~E(x411,x412)+E(f35(x413,x411),f35(x413,x412)) % 0.52/0.66 [42]~P1(x421)+P1(x422)+~E(x421,x422) % 0.52/0.66 [43]P2(x432,x433,x434)+~E(x431,x432)+~P2(x431,x433,x434) % 0.52/0.66 [44]P2(x443,x442,x444)+~E(x441,x442)+~P2(x443,x441,x444) % 0.52/0.66 [45]P2(x453,x454,x452)+~E(x451,x452)+~P2(x453,x454,x451) % 0.52/0.66 % 0.52/0.66 %------------------------------------------- % 0.52/0.66 cnf(152,plain, % 0.52/0.66 ($false), % 0.52/0.66 inference(scs_inference,[],[62,59,58,130]), % 0.52/0.66 ['proof']). % 0.52/0.66 % SZS output end Proof % 0.52/0.66 % Total time :0.000000s %------------------------------------------------------------------------------