%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ITP020+1 : TPTP v8.2.0. Bugfixed v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n032.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:11 EDT 2024 % Result : Theorem 0.48s 0.61s % Output : CNFRefutation 0.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : ITP020+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.05/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.28 % Computer : n032.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 300 % 0.09/0.28 % DateTime : Wed Jun 19 02:54:08 EDT 2024 % 0.09/0.28 % CPUTime : % 0.13/0.51 start to proof:theBenchmark % 0.48/0.59 %------------------------------------------- % 0.48/0.59 % File :CSE---1.7 % 0.48/0.59 % Problem :theBenchmark % 0.48/0.59 % Transform :cnf % 0.48/0.59 % Format :tptp:raw % 0.48/0.59 % Command :java -jar mcs_scs.jar %d %s % 0.48/0.59 % 0.48/0.59 % Result :Theorem 0.000000s % 0.48/0.59 % Output :CNFRefutation 0.000000s % 0.48/0.59 %------------------------------------------- % 0.48/0.59 %------------------------------------------------------------------------------ % 0.48/0.59 % File : ITP020+1 : TPTP v8.2.0. Bugfixed v7.5.0. % 0.48/0.59 % Domain : Interactive Theorem Proving % 0.48/0.59 % Problem : HOL4 syntactic export of thm_2Eutil__prob_2ENUM__2D__BIJ__INV.p, bushy mode % 0.48/0.59 % Version : [BG+19] axioms. % 0.48/0.59 % English : % 0.48/0.59 % 0.48/0.59 % Refs : [BG+19] Brown et al. (2019), GRUNGE: A Grand Unified ATP Chall % 0.48/0.59 % : [Gau19] Gauthier (2019), Email to Geoff Sutcliffe % 0.48/0.59 % Source : [BG+19] % 0.48/0.59 % Names : thm_2Eutil__prob_2ENUM__2D__BIJ__INV.p [Gau19] % 0.48/0.59 % : HL409501+1.p [TPAP] % 0.48/0.59 % 0.48/0.59 % Status : Theorem % 0.48/0.59 % Rating : 0.42 v8.1.0, 0.39 v7.5.0 % 0.48/0.59 % Syntax : Number of formulae : 59 ( 15 unt; 0 def) % 0.48/0.59 % Number of atoms : 209 ( 25 equ) % 0.48/0.59 % Maximal formula atoms : 15 ( 3 avg) % 0.48/0.59 % Number of connectives : 192 ( 42 ~; 38 |; 30 &) % 0.48/0.59 % ( 51 <=>; 31 =>; 0 <=; 0 <~>) % 0.48/0.59 % Maximal formula depth : 11 ( 5 avg) % 0.48/0.59 % Maximal term depth : 13 ( 2 avg) % 0.48/0.59 % Number of predicates : 2 ( 1 usr; 0 prp; 1-2 aty) % 0.48/0.59 % Number of functors : 30 ( 30 usr; 17 con; 0-3 aty) % 0.48/0.59 % Number of variables : 160 ( 144 !; 16 ?) % 0.48/0.59 % SPC : FOF_THM_RFO_SEQ % 0.48/0.59 % 0.48/0.59 % Comments : % 0.48/0.59 % Bugfixes : v7.5.0 - Bugfixes in axioms and export. % 0.48/0.59 %------------------------------------------------------------------------------ % 0.48/0.59 fof(reserved_2Eho_2Eeq__ext,axiom, % 0.48/0.59 ! [A_27a,A_27b,V0f_2E0,V1g_2E0] : % 0.48/0.59 ( ! [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.48/0.59 => s(tyop_2Emin_2Efun(A_27a,A_27b),V0f_2E0) = s(tyop_2Emin_2Efun(A_27a,A_27b),V1g_2E0) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Eboolext,axiom, % 0.48/0.59 ! [V0_2E0,V1_2E0] : % 0.48/0.59 ( ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.48/0.59 <=> p(s(tyop_2Emin_2Ebool,V1_2E0)) ) % 0.48/0.59 => s(tyop_2Emin_2Ebool,V0_2E0) = s(tyop_2Emin_2Ebool,V1_2E0) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Etruth,axiom, % 0.48/0.59 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Enotfalse,axiom, % 0.48/0.59 ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Ebool__cases__ax,axiom, % 0.48/0.59 ! [V0t_2E0] : % 0.48/0.59 ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.48/0.59 | s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Ei__thm,axiom, % 0.48/0.59 ! [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.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Ek__thm,axiom, % 0.48/0.59 ! [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.48/0.59 % 0.48/0.59 fof(reserved_2Eho_2Es__thm,axiom, % 0.48/0.59 ! [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.48/0.59 % 0.48/0.59 fof(reserved_2Elogic_2E_2F_5C,axiom, % 0.48/0.59 ! [V0_2E0,V1_2E0] : % 0.48/0.59 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_2F_5C_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.48/0.59 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.48/0.59 & p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Elogic_2E_5C_2F,axiom, % 0.48/0.59 ! [V0_2E0,V1_2E0] : % 0.48/0.59 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_5C_2F_2E2(s(tyop_2Emin_2Ebool,V0_2E0),s(tyop_2Emin_2Ebool,V1_2E0)))) % 0.48/0.59 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.48/0.59 | p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Elogic_2E_7E,axiom, % 0.48/0.59 ! [V0_2E0] : % 0.48/0.59 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_7E_2E1(s(tyop_2Emin_2Ebool,V0_2E0)))) % 0.48/0.59 <=> ~ p(s(tyop_2Emin_2Ebool,V0_2E0)) ) ). % 0.48/0.59 % 0.48/0.59 fof(reserved_2Elogic_2E_3D_3D_3E,axiom, % 0.48/0.59 ! [V0_2E0,V1_2E0] : % 0.48/0.59 ( 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.48/0.59 <=> ( p(s(tyop_2Emin_2Ebool,V0_2E0)) % 0.48/0.59 => p(s(tyop_2Emin_2Ebool,V1_2E0)) ) ) ). % 0.48/0.59 % 0.48/0.60 fof(reserved_2Elogic_2E_3D,axiom, % 0.48/0.60 ! [A_27a,V0_2E0,V1_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,c_2Emin_2E_3D_2E2(s(A_27a,V0_2E0),s(A_27a,V1_2E0)))) % 0.48/0.60 <=> s(A_27a,V0_2E0) = s(A_27a,V1_2E0) ) ). % 0.48/0.60 % 0.48/0.60 fof(reserved_2Equant_2E_21,axiom, % 0.48/0.60 ! [A_27a,V0f_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_21_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.48/0.60 <=> ! [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.48/0.60 % 0.48/0.60 fof(reserved_2Equant_2E_3F,axiom, % 0.48/0.60 ! [A_27a,V0f_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2E_3F_2E1(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0f_2E0)))) % 0.48/0.60 <=> ? [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.48/0.60 % 0.48/0.60 fof(arityeq2_2Ec_2Ebool_2E_2F_5C_2E2,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.48/0.60 <=> 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.48/0.60 % 0.48/0.60 fof(arityeq2_2Ec_2Ebool_2E_5C_2F_2E2,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.48/0.60 | p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.48/0.60 <=> 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.48/0.60 % 0.48/0.60 fof(arityeq1_2Ec_2Ebool_2E_7E_2E1,axiom, % 0.48/0.60 ! [X0_2E0] : % 0.48/0.60 ( ~ p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.48/0.60 <=> 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.48/0.60 % 0.48/0.60 fof(arityeq2_2Ec_2Emin_2E_3D_3D_3E_2E2,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,X0_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,X1_2E0)) ) % 0.48/0.60 <=> 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.48/0.60 % 0.48/0.60 fof(arityeq2_2Ec_2Emin_2E_3D_2E2_2Emono_2EA_27a,axiom, % 0.48/0.60 ! [A_27a,X0_2E0,X1_2E0] : % 0.48/0.60 ( s(A_27a,X0_2E0) = s(A_27a,X1_2E0) % 0.48/0.60 <=> 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.48/0.60 % 0.48/0.60 fof(arityeq1_2Ec_2Ebool_2E_21_2E1_2Emono_2EA_27a,axiom, % 0.48/0.60 ! [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.48/0.60 % 0.48/0.60 fof(arityeq1_2Ec_2Ebool_2E_3F_2E1_2Emono_2EA_27a,axiom, % 0.48/0.60 ! [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.48/0.60 % 0.48/0.60 fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27a_20mono_2EA_27b,axiom, % 0.48/0.60 ! [A_27a,A_27b,X0_2E0,X1_2E0,X2_2E0] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X2_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,A_27b),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(A_27a,A_27b),X0_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X1_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X2_2E0))) ). % 0.48/0.60 % 0.48/0.60 fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2EA_27b_20mono_2EA_27a,axiom, % 0.48/0.60 ! [A_27a,A_27b,X0_2E0,X1_2E0,X2_2E0] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),X0_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X2_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,A_27a),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(A_27b,A_27a),X0_2E0))),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),X1_2E0))),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),X2_2E0))) ). % 0.48/0.60 % 0.48/0.60 fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0,X2_2E0] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X2_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),X0_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1_2E0))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X2_2E0))) ). % 0.48/0.60 % 0.48/0.60 fof(arityeq2_2Ec_2Epred__set_2ECROSS_2E2_2Emono_2Etyop_2Enum_2Enum_20mono_2Etyop_2Enum_2Enum,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0] : s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X0_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1_2E0))) = s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool))),c_2Epred__set_2ECROSS_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X0_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X1_2E0))) ). % 0.48/0.60 % 0.48/0.60 fof(arityeq3_2Ec_2Epred__set_2EBIJ_2E3_2Emono_2Etyop_2Epair_2Eprod_28tyop_2Enum_2Enum_2Ctyop_2Enum_2Enum_29_20mono_2Etyop_2Enum_2Enum,axiom, % 0.48/0.60 ! [X0_2E0,X1_2E0,X2_2E0] : s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X0_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X1_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2_2E0))) = s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool)),app_2E2(s(tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),tyop_2Emin_2Efun(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),tyop_2Emin_2Ebool))),c_2Epred__set_2EBIJ_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),X0_2E0))),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),X1_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),X2_2E0))) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ETRUTH,axiom, % 0.48/0.60 p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EIMP__ANTISYM__AX,axiom, % 0.48/0.60 ! [V0t1_2E0,V1t2_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,V0t1_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,V1t2_2E0)) ) % 0.48/0.60 => ( ( p(s(tyop_2Emin_2Ebool,V1t2_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,V0t1_2E0)) ) % 0.48/0.60 => s(tyop_2Emin_2Ebool,V0t1_2E0) = s(tyop_2Emin_2Ebool,V1t2_2E0) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EIMP__F,axiom, % 0.48/0.60 ! [V0t_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.60 => ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EF__IMP,axiom, % 0.48/0.60 ! [V0t_2E0] : % 0.48/0.60 ( ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EIMP__CLAUSES,axiom, % 0.48/0.60 ! [V0t_2E0] : % 0.48/0.60 ( ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.48/0.60 & ( ( p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.48/0.60 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) % 0.48/0.60 & ( ( p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.60 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ENOT__CLAUSES,axiom, % 0.48/0.60 ( ! [V0t_2E0] : % 0.48/0.60 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.60 & ( ~ p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EEQ__SYM__EQ,axiom, % 0.48/0.60 ! [A_27a,V0x_2E0,V1y_2E0] : % 0.48/0.60 ( s(A_27a,V0x_2E0) = s(A_27a,V1y_2E0) % 0.48/0.60 <=> s(A_27a,V1y_2E0) = s(A_27a,V0x_2E0) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2EEQ__CLAUSES,axiom, % 0.48/0.60 ! [V0t_2E0] : % 0.48/0.60 ( ( s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2ET_2E0) % 0.48/0.60 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 & ( s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) = s(tyop_2Emin_2Ebool,V0t_2E0) % 0.48/0.60 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) % 0.48/0.60 & ( s(tyop_2Emin_2Ebool,V0t_2E0) = s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0) % 0.48/0.60 <=> ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ENOT__EXISTS__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0] : % 0.48/0.60 ( ~ ? [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.48/0.60 <=> ! [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.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ELEFT__AND__FORALL__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ( ! [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.48/0.60 & p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) % 0.48/0.60 <=> ! [V3x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V3x_2E0)))) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ERIGHT__AND__FORALL__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.60 & ! [V2x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V2x_2E0)))) ) % 0.48/0.60 <=> ! [V3x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V3x_2E0)))) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ELEFT__OR__EXISTS__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ( ? [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.48/0.60 | p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) % 0.48/0.60 <=> ? [V3x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V3x_2E0)))) % 0.48/0.60 | p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ERIGHT__OR__EXISTS__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.60 | ? [V2x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V2x_2E0)))) ) % 0.48/0.60 <=> ? [V3x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.60 | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V3x_2E0)))) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ELEFT__EXISTS__AND__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ? [V2x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V2x_2E0)))) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) % 0.48/0.60 <=> ( ? [V3x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0P_2E0),s(A_27a,V3x_2E0)))) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,V1Q_2E0)) ) ) ). % 0.48/0.60 % 0.48/0.60 fof(thm_2Ebool_2ERIGHT__EXISTS__AND__THM,axiom, % 0.48/0.60 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.60 ( ? [V2x_2E0] : % 0.48/0.60 ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.60 & p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V2x_2E0)))) ) % 0.48/0.60 <=> ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.61 & ? [V3x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V3x_2E0)))) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Ebool_2ELEFT__FORALL__OR__THM,axiom, % 0.48/0.61 ! [A_27a,V0Q_2E0,V1P_2E0] : % 0.48/0.61 ( ! [V2x_2E0] : % 0.48/0.61 ( p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V2x_2E0)))) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0Q_2E0)) ) % 0.48/0.61 <=> ( ! [V3x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1P_2E0),s(A_27a,V3x_2E0)))) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0Q_2E0)) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Ebool_2ERIGHT__FORALL__OR__THM,axiom, % 0.48/0.61 ! [A_27a,V0P_2E0,V1Q_2E0] : % 0.48/0.61 ( ! [V2x_2E0] : % 0.48/0.61 ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V2x_2E0)))) ) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V0P_2E0)) % 0.48/0.61 | ! [V3x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V1Q_2E0),s(A_27a,V3x_2E0)))) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Ebool_2EDISJ__SYM,axiom, % 0.48/0.61 ! [V0A_2E0,V1B_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V1B_2E0)) ) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V1B_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0A_2E0)) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Ebool_2ESKOLEM__THM,axiom, % 0.48/0.61 ! [A_27a,A_27b,V0P_2E0] : % 0.48/0.61 ( ! [V1x_2E0] : % 0.48/0.61 ? [V2y_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0P_2E0),s(A_27a,V1x_2E0))),s(A_27b,V2y_2E0)))) % 0.48/0.61 <=> ? [V3f_2E0] : % 0.48/0.61 ! [V4x_2E0] : p(s(tyop_2Emin_2Ebool,app_2E2(s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),app_2E2(s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool)),V0P_2E0),s(A_27a,V4x_2E0))),s(A_27b,app_2E2(s(tyop_2Emin_2Efun(A_27a,A_27b),V3f_2E0),s(A_27a,V4x_2E0)))))) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Epred__set_2EBIJ__SYM,axiom, % 0.48/0.61 ! [A_27a,A_27b,V0s_2E0,V1t_2E0] : % 0.48/0.61 ( ? [V2f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27a,A_27b),V2f_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0)))) % 0.48/0.61 <=> ? [V3g_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(A_27b,A_27a),V3g_2E0),s(tyop_2Emin_2Efun(A_27b,tyop_2Emin_2Ebool),V1t_2E0),s(tyop_2Emin_2Efun(A_27a,tyop_2Emin_2Ebool),V0s_2E0)))) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2ENOT__NOT,axiom, % 0.48/0.61 ! [V0t_2E0] : % 0.48/0.61 ( ~ ~ p(s(tyop_2Emin_2Ebool,V0t_2E0)) % 0.48/0.61 <=> p(s(tyop_2Emin_2Ebool,V0t_2E0)) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2EAND__INV__IMP,axiom, % 0.48/0.61 ! [V0A_2E0] : % 0.48/0.61 ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.48/0.61 => ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2EOR__DUAL2,axiom, % 0.48/0.61 ! [V0B_2E0,V1A_2E0] : % 0.48/0.61 ( ( ~ ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.61 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2EOR__DUAL3,axiom, % 0.48/0.61 ! [V0B_2E0,V1A_2E0] : % 0.48/0.61 ( ( ~ ( ~ p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0B_2E0)) ) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V1A_2E0)) % 0.48/0.61 => ( ~ p(s(tyop_2Emin_2Ebool,V0B_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2EAND__INV2,axiom, % 0.48/0.61 ! [V0A_2E0] : % 0.48/0.61 ( ( ~ p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.61 => ( ( p(s(tyop_2Emin_2Ebool,V0A_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,c_2Ebool_2EF_2E0)) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2Edc__eq,axiom, % 0.48/0.61 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 <=> s(tyop_2Emin_2Ebool,V1q_2E0) = s(tyop_2Emin_2Ebool,V0r_2E0) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2Edc__conj,axiom, % 0.48/0.61 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 & p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2Edc__disj,axiom, % 0.48/0.61 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2Edc__imp,axiom, % 0.48/0.61 ! [V0r_2E0,V1q_2E0,V2p_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 <=> ( p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 => p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V1q_2E0)) ) % 0.48/0.61 & ( p(s(tyop_2Emin_2Ebool,V2p_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V0r_2E0)) ) % 0.48/0.61 & ( ~ p(s(tyop_2Emin_2Ebool,V1q_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0r_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V2p_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Esat_2Edc__neg,axiom, % 0.48/0.61 ! [V0q_2E0,V1p_2E0] : % 0.48/0.61 ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 0.48/0.61 <=> ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 0.48/0.61 <=> ( ( p(s(tyop_2Emin_2Ebool,V1p_2E0)) % 0.48/0.61 | p(s(tyop_2Emin_2Ebool,V0q_2E0)) ) % 0.48/0.61 & ( ~ p(s(tyop_2Emin_2Ebool,V0q_2E0)) % 0.48/0.61 | ~ p(s(tyop_2Emin_2Ebool,V1p_2E0)) ) ) ) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Eutil__prob_2ENUM__2D__BIJ,axiom, % 0.48/0.61 ? [V0f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Enum_2Enum),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0))),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))) ). % 0.48/0.61 % 0.48/0.61 fof(thm_2Eutil__prob_2ENUM__2D__BIJ__INV,conjecture, % 0.48/0.61 ? [V0f_2E0] : p(s(tyop_2Emin_2Ebool,c_2Epred__set_2EBIJ_2E3(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum)),V0f_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Epair_2Eprod(tyop_2Enum_2Enum,tyop_2Enum_2Enum),tyop_2Emin_2Ebool),c_2Epred__set_2ECROSS_2E2(s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0),s(tyop_2Emin_2Efun(tyop_2Enum_2Enum,tyop_2Emin_2Ebool),c_2Epred__set_2EUNIV_2E0)))))) ). % 0.48/0.61 % 0.48/0.61 %------------------------------------------------------------------------------ % 0.48/0.61 %------------------------------------------- % 0.48/0.61 % Proof found % 0.48/0.61 % SZS status Theorem for theBenchmark % 0.48/0.61 % SZS output start Proof % 0.48/0.61 %ClaNum:228(EqnAxiom:113) % 0.48/0.61 %VarNum:627(SingletonVarNum:229) % 0.48/0.61 %MaxLitNum:4 % 0.48/0.61 %MaxfuncDepth:6 % 0.48/0.61 %SharedTerms:52 % 0.48/0.61 %goalClause: 129 % 0.48/0.61 %singleGoalClaCount:1 % 0.48/0.61 [116]P1(f5(a1,a2)) % 0.48/0.61 [128]~P1(f5(a1,a4)) % 0.48/0.61 [121]P1(f5(a1,f15(f5(f56(f58(a57,a57),a57),a27),f5(f56(f58(a57,a57),a1),f14(f5(f56(a57,a1),a13),f5(f56(a57,a1),a13))),f5(f56(a57,a1),a13)))) % 0.48/0.61 [129]~P1(f5(a1,f15(f5(f56(a57,f58(a57,a57)),x1291),f5(f56(a57,a1),a13),f5(f56(f58(a57,a57),a1),f14(f5(f56(a57,a1),a13),f5(f56(a57,a1),a13)))))) % 0.48/0.61 [117]E(f5(x1171,f3(f5(f56(x1171,x1171),a6),f5(x1171,x1172))),f5(x1171,x1172)) % 0.48/0.61 [118]E(f5(a1,f3(f5(f56(f56(x1181,a1),a1),a7),f5(f56(x1181,a1),x1182))),f5(a1,f8(f5(f56(x1181,a1),x1182)))) % 0.48/0.61 [119]E(f5(a1,f3(f5(f56(f56(x1191,a1),a1),a9),f5(f56(x1191,a1),x1192))),f5(a1,f12(f5(f56(x1191,a1),x1192)))) % 0.48/0.61 [122]E(f5(f56(f58(a57,a57),a1),f3(f5(f56(f56(a57,a1),f56(f58(a57,a57),a1)),f3(f5(f56(f56(a57,a1),f56(f56(a57,a1),f56(f58(a57,a57),a1))),a25),f5(f56(a57,a1),x1221))),f5(f56(a57,a1),x1222))),f5(f56(f58(a57,a57),a1),f14(f5(f56(a57,a1),x1221),f5(f56(a57,a1),x1222)))) % 0.48/0.61 [120]E(f5(x1201,f3(f5(f56(x1202,x1201),f3(f5(f56(x1201,f56(x1202,x1201)),a26),f5(x1201,x1203))),f5(x1202,x1204))),f5(x1201,x1203)) % 0.48/0.61 [124]E(f5(a1,f3(f5(f56(f56(x1241,a1),a1),f3(f5(f56(f56(x1242,a1),f56(f56(x1241,a1),a1)),f3(f5(f56(f56(x1242,x1241),f56(f56(x1242,a1),f56(f56(x1241,a1),a1))),a16),f5(f56(x1242,x1241),x1243))),f5(f56(x1242,a1),x1244))),f5(f56(x1241,a1),x1245))),f5(a1,f15(f5(f56(x1242,x1241),x1243),f5(f56(x1242,a1),x1244),f5(f56(x1241,a1),x1245)))) % 0.48/0.61 [125]E(f5(x1251,f3(f5(f56(x1252,x1251),f3(f5(f56(f56(x1252,x1253),f56(x1252,x1251)),f3(f5(f56(f56(x1252,f56(x1253,x1251)),f56(f56(x1252,x1253),f56(x1252,x1251))),a28),f5(f56(x1252,f56(x1253,x1251)),x1254))),f5(f56(x1252,x1253),x1255))),f5(x1252,x1256))),f5(x1251,f3(f5(f56(x1253,x1251),f3(f5(f56(x1252,f56(x1253,x1251)),x1254),f5(x1252,x1256))),f5(x1253,f3(f5(f56(x1252,x1253),x1255),f5(x1252,x1256)))))) % 0.48/0.61 [130]E(f5(a1,x1301),f5(a1,a2))+E(f5(a1,x1301),f5(a1,a4)) % 0.48/0.61 [134]E(f5(a1,x1341),f5(a1,a4))+P1(f5(a1,x1341)) % 0.48/0.61 [135]E(f5(a1,a4),f5(a1,x1351))+P1(f5(a1,x1351)) % 0.48/0.61 [138]~E(f5(a1,x1381),f5(a1,a2))+P1(f5(a1,x1381)) % 0.48/0.61 [139]~E(f5(a1,a2),f5(a1,x1391))+P1(f5(a1,x1391)) % 0.48/0.61 [140]E(f5(a1,x1401),f5(a1,a2))+~P1(f5(a1,x1401)) % 0.48/0.61 [141]E(f5(a1,a2),f5(a1,x1411))+~P1(f5(a1,x1411)) % 0.48/0.61 [147]~E(f5(a1,x1471),f5(a1,a4))+~P1(f5(a1,x1471)) % 0.48/0.61 [148]~E(f5(a1,a4),f5(a1,x1481))+~P1(f5(a1,x1481)) % 0.48/0.61 [166]P1(f5(a1,x1661))+P1(f5(a1,f17(f5(a1,x1661)))) % 0.48/0.61 [177]~P1(f5(a1,x1771))+~P1(f5(a1,f17(f5(a1,x1771)))) % 0.48/0.61 [186]P1(f5(a1,x1861))+P1(f5(a1,f3(f5(f56(a1,a1),a20),f5(a1,x1861)))) % 0.48/0.61 [190]~P1(f5(a1,x1901))+~P1(f5(a1,f3(f5(f56(a1,a1),a20),f5(a1,x1901)))) % 0.48/0.61 [178]P1(f5(a1,x1781))+P1(f5(a1,f21(f5(a1,x1781),f5(a1,x1782)))) % 0.48/0.61 [179]~P1(f5(a1,x1792))+P1(f5(a1,f18(f5(a1,x1791),f5(a1,x1792)))) % 0.48/0.61 [180]~P1(f5(a1,x1801))+P1(f5(a1,f18(f5(a1,x1801),f5(a1,x1802)))) % 0.48/0.61 [181]~P1(f5(a1,x1812))+P1(f5(a1,f21(f5(a1,x1811),f5(a1,x1812)))) % 0.48/0.61 [184]P1(f5(a1,x1841))+~P1(f5(a1,f10(f5(a1,x1842),f5(a1,x1841)))) % 0.48/0.61 [185]P1(f5(a1,x1851))+~P1(f5(a1,f10(f5(a1,x1851),f5(a1,x1852)))) % 0.48/0.61 [213]P1(f5(a1,x2131))+P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a24),f5(a1,x2131))),f5(a1,x2132)))) % 0.48/0.61 [214]~P1(f5(a1,x2142))+P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a19),f5(a1,x2141))),f5(a1,x2142)))) % 0.48/0.61 [215]~P1(f5(a1,x2151))+P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a19),f5(a1,x2151))),f5(a1,x2152)))) % 0.48/0.61 [216]~P1(f5(a1,x2162))+P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a24),f5(a1,x2161))),f5(a1,x2162)))) % 0.48/0.61 [219]P1(f5(a1,x2191))+~P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a11),f5(a1,x2192))),f5(a1,x2191)))) % 0.48/0.61 [220]P1(f5(a1,x2201))+~P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a11),f5(a1,x2201))),f5(a1,x2202)))) % 0.48/0.61 [193]P1(f5(a1,f3(f5(f56(x1931,a1),x1932),f5(x1931,f48(x1931,x1932)))))+~P1(f5(a1,f12(f5(f56(x1931,a1),x1932)))) % 0.48/0.61 [194]~P1(f5(a1,f3(f5(f56(x1941,a1),x1942),f5(x1941,f49(x1941,x1942)))))+P1(f5(a1,f8(f5(f56(x1941,a1),x1942)))) % 0.48/0.61 [182]~E(f5(x1821,x1822),f5(x1821,x1823))+P1(f5(a1,f22(f5(x1821,x1822),f5(x1821,x1823)))) % 0.48/0.61 [188]E(f5(x1881,x1882),f5(x1881,x1883))+~P1(f5(a1,f22(f5(x1881,x1882),f5(x1881,x1883)))) % 0.48/0.61 [218]~E(f5(x2181,x2182),f5(x2181,x2183))+P1(f5(a1,f3(f5(f56(x2181,a1),f3(f5(f56(x2181,f56(x2181,a1)),a23),f5(x2181,x2182))),f5(x2181,x2183)))) % 0.48/0.61 [223]E(f5(x2231,x2232),f5(x2231,x2233))+~P1(f5(a1,f3(f5(f56(x2231,a1),f3(f5(f56(x2231,f56(x2231,a1)),a23),f5(x2231,x2232))),f5(x2231,x2233)))) % 0.48/0.61 [191]P1(f5(a1,f3(f5(f56(x1911,a1),x1912),f5(x1911,x1913))))+~P1(f5(a1,f8(f5(f56(x1911,a1),x1912)))) % 0.48/0.61 [192]~P1(f5(a1,f3(f5(f56(x1921,a1),x1922),f5(x1921,x1923))))+P1(f5(a1,f12(f5(f56(x1921,a1),x1922)))) % 0.48/0.61 [195]~P1(f5(a1,f3(f5(f56(x1951,a1),x1952),f5(x1951,x1953))))+P1(f5(a1,f3(f5(f56(x1951,a1),x1952),f5(x1951,f50(x1951,x1952))))) % 0.48/0.61 [196]~P1(f5(a1,f3(f5(f56(x1961,a1),x1962),f5(x1961,x1963))))+P1(f5(a1,f3(f5(f56(x1961,a1),x1962),f5(x1961,f51(x1961,x1962))))) % 0.48/0.61 [226]E(f5(f56(x2261,x2262),x2263),f5(f56(x2261,x2262),x2264))+~E(f5(x2262,f3(f5(f56(x2261,x2262),x2263),f5(x2261,f40(x2261,x2262,x2263,x2264)))),f5(x2262,f3(f5(f56(x2261,x2262),x2264),f5(x2261,f40(x2261,x2262,x2263,x2264))))) % 0.48/0.61 [224]~P1(f5(a1,f15(f5(f56(x2242,x2241),x2245),f5(f56(x2242,a1),x2243),f5(f56(x2241,a1),x2244))))+P1(f5(a1,f15(f5(f56(x2241,x2242),f42(x2242,x2241,x2243,x2244)),f5(f56(x2241,a1),x2244),f5(f56(x2242,a1),x2243)))) % 0.48/0.61 [225]~P1(f5(a1,f15(f5(f56(x2252,x2251),x2255),f5(f56(x2252,a1),x2254),f5(f56(x2251,a1),x2253))))+P1(f5(a1,f15(f5(f56(x2251,x2252),f47(x2251,x2252,x2253,x2254)),f5(f56(x2251,a1),x2253),f5(f56(x2252,a1),x2254)))) % 0.48/0.61 [227]~P1(f5(a1,f3(f5(f56(x2271,a1),f3(f5(f56(x2272,f56(x2271,a1)),x2273),f5(x2272,f44(x2272,x2271,x2273)))),f5(x2271,x2275))))+P1(f5(a1,f3(f5(f56(x2271,a1),f3(f5(f56(x2272,f56(x2271,a1)),x2273),f5(x2272,x2274))),f5(x2271,f3(f5(f56(x2272,x2271),f43(x2272,x2271,x2273)),f5(x2272,x2274)))))) % 0.48/0.61 [228]P1(f5(a1,f3(f5(f56(x2281,a1),f3(f5(f56(x2282,f56(x2281,a1)),x2283),f5(x2282,x2284))),f5(x2281,f45(x2282,x2281,x2283,x2284)))))+~P1(f5(a1,f3(f5(f56(x2281,a1),f3(f5(f56(x2282,f56(x2281,a1)),x2283),f5(x2282,f46(x2282,x2281,x2283,x2285)))),f5(x2281,f3(f5(f56(x2282,x2281),x2285),f5(x2282,f46(x2282,x2281,x2283,x2285))))))) % 0.48/0.61 [146]E(f5(a1,x1461),f5(a1,x1462))+P1(f5(a1,x1461))+P1(f5(a1,x1462)) % 0.48/0.61 [154]E(f5(a1,x1541),f5(a1,x1542))+~P1(f5(a1,x1541))+~P1(f5(a1,x1542)) % 0.48/0.61 [183]~P1(f5(a1,x1831))+~P1(f5(a1,x1832))+P1(f5(a1,f10(f5(a1,x1831),f5(a1,x1832)))) % 0.48/0.61 [187]P1(f5(a1,x1871))+P1(f5(a1,x1872))+~P1(f5(a1,f18(f5(a1,x1872),f5(a1,x1871)))) % 0.48/0.61 [189]P1(f5(a1,x1891))+~P1(f5(a1,x1892))+~P1(f5(a1,f21(f5(a1,x1892),f5(a1,x1891)))) % 0.48/0.61 [217]~P1(f5(a1,x2171))+~P1(f5(a1,x2172))+P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a11),f5(a1,x2171))),f5(a1,x2172)))) % 0.48/0.61 [221]P1(f5(a1,x2211))+P1(f5(a1,x2212))+~P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a19),f5(a1,x2212))),f5(a1,x2211)))) % 0.48/0.61 [222]P1(f5(a1,x2221))+~P1(f5(a1,x2222))+~P1(f5(a1,f3(f5(f56(a1,a1),f3(f5(f56(a1,f56(a1,a1)),a24),f5(a1,x2222))),f5(a1,x2221)))) % 0.48/0.61 [152]P2(x1523,x1521,x1522)+E(f5(a1,x1521),f5(a1,x1522))+P1(f5(a1,x1523)) % 0.48/0.61 [156]P2(x1561,x1562,x1563)+P1(f5(a1,x1563))+~P1(f5(a1,x1562)) % 0.48/0.61 [158]P2(x1581,x1582,x1583)+P1(f5(a1,x1583))+~P1(f5(a1,x1581)) % 0.48/0.61 [159]P2(x1591,x1592,x1593)+~E(f5(a1,x1592),f5(a1,x1593))+~P1(f5(a1,x1591)) % 0.48/0.61 [161]P2(x1611,x1612,x1613)+~P1(f5(a1,x1611))+~P1(f5(a1,x1612)) % 0.48/0.61 [165]~P2(x1651,x1652,x1653)+~E(f5(a1,x1652),f5(a1,x1653))+P1(f5(a1,x1651)) % 0.48/0.61 [197]P1(f5(a1,x1971))+~P1(f5(a1,f3(f5(f56(x1972,a1),x1973),f5(x1972,x1974))))+P1(f5(a1,f3(f5(f56(x1972,a1),x1973),f5(x1972,f29(x1972,x1973,x1971))))) % 0.48/0.61 [198]P1(f5(a1,x1981))+~P1(f5(a1,f3(f5(f56(x1982,a1),x1983),f5(x1982,x1984))))+P1(f5(a1,f3(f5(f56(x1982,a1),x1983),f5(x1982,f30(x1982,x1983,x1981))))) % 0.48/0.61 [199]P1(f5(a1,x1991))+~P1(f5(a1,f3(f5(f56(x1992,a1),x1993),f5(x1992,x1994))))+P1(f5(a1,f3(f5(f56(x1992,a1),x1993),f5(x1992,f31(x1992,x1991,x1993))))) % 0.48/0.61 [200]P1(f5(a1,x2001))+~P1(f5(a1,f3(f5(f56(x2002,a1),x2003),f5(x2002,x2004))))+P1(f5(a1,f3(f5(f56(x2002,a1),x2003),f5(x2002,f32(x2002,x2001,x2003))))) % 0.48/0.61 [201]~P1(f5(a1,x2013))+~P1(f5(a1,f3(f5(f56(x2011,a1),x2012),f5(x2011,x2014))))+P1(f5(a1,f3(f5(f56(x2011,a1),x2012),f5(x2011,f33(x2011,x2012,x2013))))) % 0.48/0.61 [202]~P1(f5(a1,x2023))+~P1(f5(a1,f3(f5(f56(x2021,a1),x2022),f5(x2021,x2024))))+P1(f5(a1,f3(f5(f56(x2021,a1),x2022),f5(x2021,f34(x2021,x2022,x2023))))) % 0.48/0.61 [203]~P1(f5(a1,x2033))+~P1(f5(a1,f3(f5(f56(x2031,a1),x2032),f5(x2031,x2034))))+P1(f5(a1,f3(f5(f56(x2031,a1),x2032),f5(x2031,f35(x2031,x2033,x2032))))) % 0.48/0.61 [204]~P1(f5(a1,x2043))+~P1(f5(a1,f3(f5(f56(x2041,a1),x2042),f5(x2041,x2044))))+P1(f5(a1,f3(f5(f56(x2041,a1),x2042),f5(x2041,f36(x2041,x2043,x2042))))) % 0.48/0.61 [205]P1(f5(a1,x2051))+P1(f5(a1,f3(f5(f56(x2052,a1),x2053),f5(x2052,x2054))))+~P1(f5(a1,f3(f5(f56(x2052,a1),x2053),f5(x2052,f37(x2052,x2051,x2053))))) % 0.48/0.61 [206]P1(f5(a1,x2061))+P1(f5(a1,f3(f5(f56(x2062,a1),x2063),f5(x2062,x2064))))+~P1(f5(a1,f3(f5(f56(x2062,a1),x2063),f5(x2062,f38(x2062,x2061,x2063))))) % 0.48/0.61 [207]P1(f5(a1,x2071))+P1(f5(a1,f3(f5(f56(x2072,a1),x2073),f5(x2072,x2074))))+~P1(f5(a1,f3(f5(f56(x2072,a1),x2073),f5(x2072,f39(x2072,x2071,x2073))))) % 0.48/0.61 [208]P1(f5(a1,x2081))+P1(f5(a1,f3(f5(f56(x2082,a1),x2083),f5(x2082,x2084))))+~P1(f5(a1,f3(f5(f56(x2082,a1),x2083),f5(x2082,f41(x2082,x2081,x2083))))) % 0.48/0.61 [209]~P1(f5(a1,x2094))+P1(f5(a1,f3(f5(f56(x2091,a1),x2092),f5(x2091,x2093))))+~P1(f5(a1,f3(f5(f56(x2091,a1),x2092),f5(x2091,f52(x2091,x2092,x2094))))) % 0.48/0.61 [210]~P1(f5(a1,x2104))+P1(f5(a1,f3(f5(f56(x2101,a1),x2102),f5(x2101,x2103))))+~P1(f5(a1,f3(f5(f56(x2101,a1),x2102),f5(x2101,f53(x2101,x2102,x2104))))) % 0.48/0.61 [211]~P1(f5(a1,x2114))+P1(f5(a1,f3(f5(f56(x2111,a1),x2112),f5(x2111,x2113))))+~P1(f5(a1,f3(f5(f56(x2111,a1),x2112),f5(x2111,f54(x2111,x2114,x2112))))) % 0.48/0.61 [212]~P1(f5(a1,x2124))+P1(f5(a1,f3(f5(f56(x2121,a1),x2122),f5(x2121,x2123))))+~P1(f5(a1,f3(f5(f56(x2121,a1),x2122),f5(x2121,f55(x2121,x2124,x2122))))) % 0.48/0.61 [164]P2(x1641,x1642,x1643)+P1(f5(a1,x1642))+P1(f5(a1,x1641))+~P1(f5(a1,x1643)) % 0.48/0.61 [167]~P2(x1673,x1672,x1671)+P1(f5(a1,x1671))+P1(f5(a1,x1672))+P1(f5(a1,x1673)) % 0.48/0.61 [171]~P2(x1713,x1711,x1712)+E(f5(a1,x1711),f5(a1,x1712))+P1(f5(a1,x1711))+~P1(f5(a1,x1713)) % 0.48/0.61 [174]~P2(x1743,x1741,x1742)+E(f5(a1,x1741),f5(a1,x1742))+~P1(f5(a1,x1742))+~P1(f5(a1,x1743)) % 0.48/0.61 [175]~P2(x1752,x1751,x1753)+~P1(f5(a1,x1752))+~P1(f5(a1,x1753))+P1(f5(a1,x1751)) % 0.48/0.61 [176]~P2(x1761,x1762,x1763)+~P1(f5(a1,x1762))+~P1(f5(a1,x1763))+P1(f5(a1,x1761)) % 0.48/0.61 %EqnAxiom % 0.48/0.61 [1]E(x11,x11) % 0.48/0.61 [2]E(x22,x21)+~E(x21,x22) % 0.48/0.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.48/0.61 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 0.48/0.61 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 0.48/0.61 [6]~E(x61,x62)+E(f3(x61,x63),f3(x62,x63)) % 0.48/0.61 [7]~E(x71,x72)+E(f3(x73,x71),f3(x73,x72)) % 0.48/0.61 [8]~E(x81,x82)+E(f17(x81),f17(x82)) % 0.48/0.61 [9]~E(x91,x92)+E(f56(x91,x93),f56(x92,x93)) % 0.48/0.61 [10]~E(x101,x102)+E(f56(x103,x101),f56(x103,x102)) % 0.48/0.61 [11]~E(x111,x112)+E(f46(x111,x113,x114,x115),f46(x112,x113,x114,x115)) % 0.48/0.61 [12]~E(x121,x122)+E(f46(x123,x121,x124,x125),f46(x123,x122,x124,x125)) % 0.48/0.61 [13]~E(x131,x132)+E(f46(x133,x134,x131,x135),f46(x133,x134,x132,x135)) % 0.48/0.61 [14]~E(x141,x142)+E(f46(x143,x144,x145,x141),f46(x143,x144,x145,x142)) % 0.48/0.61 [15]~E(x151,x152)+E(f39(x151,x153,x154),f39(x152,x153,x154)) % 0.48/0.61 [16]~E(x161,x162)+E(f39(x163,x161,x164),f39(x163,x162,x164)) % 0.48/0.61 [17]~E(x171,x172)+E(f39(x173,x174,x171),f39(x173,x174,x172)) % 0.48/0.61 [18]~E(x181,x182)+E(f21(x181,x183),f21(x182,x183)) % 0.48/0.61 [19]~E(x191,x192)+E(f21(x193,x191),f21(x193,x192)) % 0.48/0.61 [20]~E(x201,x202)+E(f18(x201,x203),f18(x202,x203)) % 0.48/0.61 [21]~E(x211,x212)+E(f18(x213,x211),f18(x213,x212)) % 0.48/0.61 [22]~E(x221,x222)+E(f15(x221,x223,x224),f15(x222,x223,x224)) % 0.48/0.61 [23]~E(x231,x232)+E(f15(x233,x231,x234),f15(x233,x232,x234)) % 0.48/0.61 [24]~E(x241,x242)+E(f15(x243,x244,x241),f15(x243,x244,x242)) % 0.48/0.61 [25]~E(x251,x252)+E(f41(x251,x253,x254),f41(x252,x253,x254)) % 0.48/0.61 [26]~E(x261,x262)+E(f41(x263,x261,x264),f41(x263,x262,x264)) % 0.48/0.61 [27]~E(x271,x272)+E(f41(x273,x274,x271),f41(x273,x274,x272)) % 0.48/0.61 [28]~E(x281,x282)+E(f52(x281,x283,x284),f52(x282,x283,x284)) % 0.48/0.61 [29]~E(x291,x292)+E(f52(x293,x291,x294),f52(x293,x292,x294)) % 0.48/0.61 [30]~E(x301,x302)+E(f52(x303,x304,x301),f52(x303,x304,x302)) % 0.48/0.61 [31]~E(x311,x312)+E(f38(x311,x313,x314),f38(x312,x313,x314)) % 0.48/0.61 [32]~E(x321,x322)+E(f38(x323,x321,x324),f38(x323,x322,x324)) % 0.48/0.61 [33]~E(x331,x332)+E(f38(x333,x334,x331),f38(x333,x334,x332)) % 0.48/0.61 [34]~E(x341,x342)+E(f53(x341,x343,x344),f53(x342,x343,x344)) % 0.48/0.61 [35]~E(x351,x352)+E(f53(x353,x351,x354),f53(x353,x352,x354)) % 0.48/0.61 [36]~E(x361,x362)+E(f53(x363,x364,x361),f53(x363,x364,x362)) % 0.48/0.61 [37]~E(x371,x372)+E(f37(x371,x373,x374),f37(x372,x373,x374)) % 0.48/0.61 [38]~E(x381,x382)+E(f37(x383,x381,x384),f37(x383,x382,x384)) % 0.48/0.61 [39]~E(x391,x392)+E(f37(x393,x394,x391),f37(x393,x394,x392)) % 0.48/0.61 [40]~E(x401,x402)+E(f47(x401,x403,x404,x405),f47(x402,x403,x404,x405)) % 0.48/0.61 [41]~E(x411,x412)+E(f47(x413,x411,x414,x415),f47(x413,x412,x414,x415)) % 0.48/0.61 [42]~E(x421,x422)+E(f47(x423,x424,x421,x425),f47(x423,x424,x422,x425)) % 0.48/0.61 [43]~E(x431,x432)+E(f47(x433,x434,x435,x431),f47(x433,x434,x435,x432)) % 0.48/0.61 [44]~E(x441,x442)+E(f54(x441,x443,x444),f54(x442,x443,x444)) % 0.48/0.61 [45]~E(x451,x452)+E(f54(x453,x451,x454),f54(x453,x452,x454)) % 0.48/0.61 [46]~E(x461,x462)+E(f54(x463,x464,x461),f54(x463,x464,x462)) % 0.48/0.61 [47]~E(x471,x472)+E(f55(x471,x473,x474),f55(x472,x473,x474)) % 0.48/0.61 [48]~E(x481,x482)+E(f55(x483,x481,x484),f55(x483,x482,x484)) % 0.48/0.61 [49]~E(x491,x492)+E(f55(x493,x494,x491),f55(x493,x494,x492)) % 0.48/0.61 [50]~E(x501,x502)+E(f14(x501,x503),f14(x502,x503)) % 0.48/0.61 [51]~E(x511,x512)+E(f14(x513,x511),f14(x513,x512)) % 0.48/0.61 [52]~E(x521,x522)+E(f8(x521),f8(x522)) % 0.48/0.61 [53]~E(x531,x532)+E(f45(x531,x533,x534,x535),f45(x532,x533,x534,x535)) % 0.48/0.62 [54]~E(x541,x542)+E(f45(x543,x541,x544,x545),f45(x543,x542,x544,x545)) % 0.48/0.62 [55]~E(x551,x552)+E(f45(x553,x554,x551,x555),f45(x553,x554,x552,x555)) % 0.48/0.62 [56]~E(x561,x562)+E(f45(x563,x564,x565,x561),f45(x563,x564,x565,x562)) % 0.48/0.62 [57]~E(x571,x572)+E(f36(x571,x573,x574),f36(x572,x573,x574)) % 0.48/0.62 [58]~E(x581,x582)+E(f36(x583,x581,x584),f36(x583,x582,x584)) % 0.48/0.62 [59]~E(x591,x592)+E(f36(x593,x594,x591),f36(x593,x594,x592)) % 0.48/0.62 [60]~E(x601,x602)+E(f35(x601,x603,x604),f35(x602,x603,x604)) % 0.48/0.62 [61]~E(x611,x612)+E(f35(x613,x611,x614),f35(x613,x612,x614)) % 0.48/0.62 [62]~E(x621,x622)+E(f35(x623,x624,x621),f35(x623,x624,x622)) % 0.48/0.62 [63]~E(x631,x632)+E(f22(x631,x633),f22(x632,x633)) % 0.48/0.62 [64]~E(x641,x642)+E(f22(x643,x641),f22(x643,x642)) % 0.48/0.62 [65]~E(x651,x652)+E(f58(x651,x653),f58(x652,x653)) % 0.48/0.62 [66]~E(x661,x662)+E(f58(x663,x661),f58(x663,x662)) % 0.48/0.62 [67]~E(x671,x672)+E(f42(x671,x673,x674,x675),f42(x672,x673,x674,x675)) % 0.48/0.62 [68]~E(x681,x682)+E(f42(x683,x681,x684,x685),f42(x683,x682,x684,x685)) % 0.48/0.62 [69]~E(x691,x692)+E(f42(x693,x694,x691,x695),f42(x693,x694,x692,x695)) % 0.48/0.62 [70]~E(x701,x702)+E(f42(x703,x704,x705,x701),f42(x703,x704,x705,x702)) % 0.48/0.62 [71]~E(x711,x712)+E(f10(x711,x713),f10(x712,x713)) % 0.48/0.62 [72]~E(x721,x722)+E(f10(x723,x721),f10(x723,x722)) % 0.48/0.62 [73]~E(x731,x732)+E(f51(x731,x733),f51(x732,x733)) % 0.48/0.62 [74]~E(x741,x742)+E(f51(x743,x741),f51(x743,x742)) % 0.48/0.62 [75]~E(x751,x752)+E(f29(x751,x753,x754),f29(x752,x753,x754)) % 0.48/0.62 [76]~E(x761,x762)+E(f29(x763,x761,x764),f29(x763,x762,x764)) % 0.48/0.62 [77]~E(x771,x772)+E(f29(x773,x774,x771),f29(x773,x774,x772)) % 0.48/0.62 [78]~E(x781,x782)+E(f12(x781),f12(x782)) % 0.48/0.62 [79]~E(x791,x792)+E(f48(x791,x793),f48(x792,x793)) % 0.48/0.62 [80]~E(x801,x802)+E(f48(x803,x801),f48(x803,x802)) % 0.48/0.62 [81]~E(x811,x812)+E(f50(x811,x813),f50(x812,x813)) % 0.48/0.62 [82]~E(x821,x822)+E(f50(x823,x821),f50(x823,x822)) % 0.48/0.62 [83]~E(x831,x832)+E(f30(x831,x833,x834),f30(x832,x833,x834)) % 0.48/0.62 [84]~E(x841,x842)+E(f30(x843,x841,x844),f30(x843,x842,x844)) % 0.48/0.62 [85]~E(x851,x852)+E(f30(x853,x854,x851),f30(x853,x854,x852)) % 0.48/0.62 [86]~E(x861,x862)+E(f34(x861,x863,x864),f34(x862,x863,x864)) % 0.48/0.62 [87]~E(x871,x872)+E(f34(x873,x871,x874),f34(x873,x872,x874)) % 0.48/0.62 [88]~E(x881,x882)+E(f34(x883,x884,x881),f34(x883,x884,x882)) % 0.48/0.62 [89]~E(x891,x892)+E(f40(x891,x893,x894,x895),f40(x892,x893,x894,x895)) % 0.48/0.62 [90]~E(x901,x902)+E(f40(x903,x901,x904,x905),f40(x903,x902,x904,x905)) % 0.48/0.62 [91]~E(x911,x912)+E(f40(x913,x914,x911,x915),f40(x913,x914,x912,x915)) % 0.48/0.62 [92]~E(x921,x922)+E(f40(x923,x924,x925,x921),f40(x923,x924,x925,x922)) % 0.48/0.62 [93]~E(x931,x932)+E(f43(x931,x933,x934),f43(x932,x933,x934)) % 0.48/0.62 [94]~E(x941,x942)+E(f43(x943,x941,x944),f43(x943,x942,x944)) % 0.48/0.62 [95]~E(x951,x952)+E(f43(x953,x954,x951),f43(x953,x954,x952)) % 0.48/0.62 [96]~E(x961,x962)+E(f44(x961,x963,x964),f44(x962,x963,x964)) % 0.48/0.62 [97]~E(x971,x972)+E(f44(x973,x971,x974),f44(x973,x972,x974)) % 0.48/0.62 [98]~E(x981,x982)+E(f44(x983,x984,x981),f44(x983,x984,x982)) % 0.48/0.62 [99]~E(x991,x992)+E(f31(x991,x993,x994),f31(x992,x993,x994)) % 0.48/0.62 [100]~E(x1001,x1002)+E(f31(x1003,x1001,x1004),f31(x1003,x1002,x1004)) % 0.48/0.62 [101]~E(x1011,x1012)+E(f31(x1013,x1014,x1011),f31(x1013,x1014,x1012)) % 0.48/0.62 [102]~E(x1021,x1022)+E(f33(x1021,x1023,x1024),f33(x1022,x1023,x1024)) % 0.48/0.62 [103]~E(x1031,x1032)+E(f33(x1033,x1031,x1034),f33(x1033,x1032,x1034)) % 0.48/0.62 [104]~E(x1041,x1042)+E(f33(x1043,x1044,x1041),f33(x1043,x1044,x1042)) % 0.48/0.62 [105]~E(x1051,x1052)+E(f32(x1051,x1053,x1054),f32(x1052,x1053,x1054)) % 0.48/0.62 [106]~E(x1061,x1062)+E(f32(x1063,x1061,x1064),f32(x1063,x1062,x1064)) % 0.48/0.62 [107]~E(x1071,x1072)+E(f32(x1073,x1074,x1071),f32(x1073,x1074,x1072)) % 0.48/0.62 [108]~E(x1081,x1082)+E(f49(x1081,x1083),f49(x1082,x1083)) % 0.48/0.62 [109]~E(x1091,x1092)+E(f49(x1093,x1091),f49(x1093,x1092)) % 0.48/0.62 [110]~P1(x1101)+P1(x1102)+~E(x1101,x1102) % 0.48/0.62 [111]P2(x1112,x1113,x1114)+~E(x1111,x1112)+~P2(x1111,x1113,x1114) % 0.48/0.62 [112]P2(x1123,x1122,x1124)+~E(x1121,x1122)+~P2(x1123,x1121,x1124) % 0.48/0.62 [113]P2(x1133,x1134,x1132)+~E(x1131,x1132)+~P2(x1133,x1134,x1131) % 0.48/0.62 % 0.48/0.62 %------------------------------------------- % 0.48/0.62 cnf(238,plain, % 0.48/0.62 ($false), % 0.48/0.62 inference(scs_inference,[],[121,129,224]), % 0.48/0.62 ['proof']). % 0.48/0.62 % SZS output end Proof % 0.48/0.62 % Total time :0.000000s %------------------------------------------------------------------------------