%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SWW469+5 : TPTP v8.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n009.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 18:09:28 EDT 2024 % Result : Theorem 1.63s 1.70s % Output : CNFRefutation 1.63s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWW469+5 : TPTP v8.2.0. Released v5.3.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n009.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 : Wed Jun 19 05:45:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.55 start to proof:theBenchmark % 1.63/1.68 %------------------------------------------- % 1.63/1.68 % File :CSE---1.7 % 1.63/1.68 % Problem :theBenchmark % 1.63/1.68 % Transform :cnf % 1.63/1.68 % Format :tptp:raw % 1.63/1.68 % Command :java -jar mcs_scs.jar %d %s % 1.63/1.68 % 1.63/1.68 % Result :Theorem 1.060000s % 1.63/1.68 % Output :CNFRefutation 1.060000s % 1.63/1.68 %------------------------------------------- % 1.63/1.68 %------------------------------------------------------------------------------ % 1.63/1.68 % File : SWW469+5 : TPTP v8.2.0. Released v5.3.0. % 1.63/1.68 % Domain : Software Verification % 1.63/1.68 % Problem : Hoare's Logic with Procedures line 112, 100 axioms selected % 1.63/1.68 % Version : Especial. % 1.63/1.68 % English : % 1.63/1.68 % 1.63/1.68 % Refs : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 1.63/1.68 % : [Bla11] Blanchette (2011), Email to Geoff Sutcliffe % 1.63/1.68 % Source : [Bla11] % 1.63/1.68 % Names : hoare_100_fofpt_l112 [Bla11] % 1.63/1.68 % 1.63/1.68 % Status : Theorem % 1.63/1.68 % Rating : 0.08 v7.5.0, 0.09 v7.4.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.10 v6.4.0, 0.15 v6.3.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.10 v6.0.0, 0.09 v5.5.0, 0.22 v5.4.0, 0.25 v5.3.0 % 1.63/1.68 % Syntax : Number of formulae : 63 ( 31 unt; 0 def) % 1.63/1.68 % Number of atoms : 114 ( 45 equ) % 1.63/1.68 % Maximal formula atoms : 5 ( 1 avg) % 1.63/1.68 % Number of connectives : 64 ( 13 ~; 2 |; 3 &) % 1.63/1.68 % ( 10 <=>; 36 =>; 0 <=; 0 <~>) % 1.63/1.68 % Maximal formula depth : 12 ( 5 avg) % 1.63/1.68 % Maximal term depth : 12 ( 2 avg) % 1.63/1.68 % Number of predicates : 4 ( 3 usr; 0 prp; 1-2 aty) % 1.63/1.68 % Number of functors : 22 ( 22 usr; 6 con; 0-4 aty) % 1.63/1.68 % Number of variables : 157 ( 155 !; 2 ?) % 1.63/1.68 % SPC : FOF_THM_RFO_SEQ % 1.63/1.68 % 1.63/1.68 % Comments : This file was generated by Isabelle (most likely Sledgehammer) % 1.63/1.68 % 2011-08-09 13:53:52 % 1.63/1.68 % : Encoded with polymorphic tags. % 1.63/1.68 %------------------------------------------------------------------------------ % 1.63/1.68 %----Explicit typings (17) % 1.63/1.68 fof(tsy_c_HOL_Oequal__class_Oequal_res,axiom, % 1.63/1.68 ! [X_a] : % 1.63/1.68 ( cl_HOL_Oequal(X_a) % 1.63/1.68 => ti(fun(X_a,fun(X_a,bool)),equal_equal(X_a)) = equal_equal(X_a) ) ). % 1.63/1.68 % 1.63/1.68 fof(tsy_c_HOL_Oinduct__equal_res,axiom, % 1.63/1.68 ! [X_a] : ti(fun(X_a,fun(X_a,bool)),induct_equal(X_a)) = induct_equal(X_a) ). % 1.63/1.68 % 1.63/1.68 fof(tsy_c_HOL_Oinduct__false_res,axiom, % 1.63/1.68 ti(bool,induct_false) = induct_false ). % 1.63/1.68 % 1.63/1.69 fof(tsy_c_HOL_Oinduct__true_res,axiom, % 1.63/1.69 ti(bool,induct_true) = induct_true ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_HOL_Oundefined_res,axiom, % 1.63/1.69 ! [X_a] : ti(X_a,undefined(X_a)) = undefined(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Hoare__Mirabelle__pjuwniqynr_OAbs__triple_res,axiom, % 1.63/1.69 ! [X_a] : ti(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a)),hoare_244953527triple(X_a)) = hoare_244953527triple(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Hoare__Mirabelle__pjuwniqynr_ORep__triple_res,axiom, % 1.63/1.69 ! [X_a] : ti(fun(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_2037801986triple(X_a)) = hoare_2037801986triple(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Hoare__Mirabelle__pjuwniqynr_Ostate__not__singleton_res,hypothesis, % 1.63/1.69 ti(bool,hoare_1883395792gleton) = hoare_1883395792gleton ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Hoare__Mirabelle__pjuwniqynr_Otriple_Otriple__rep__set_res,axiom, % 1.63/1.69 ! [X_a] : ti(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),hoare_1580379338ep_set(X_a)) = hoare_1580379338ep_set(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Set_OCollect_res,axiom, % 1.63/1.69 ! [X_a] : ti(fun(fun(X_a,bool),fun(X_a,bool)),collect(X_a)) = collect(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_Typedef_Otype__definition_res,axiom, % 1.63/1.69 ! [X_a,X_b] : ti(fun(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool))),type_definition(X_a,X_b)) = type_definition(X_a,X_b) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_fequal_res,axiom, % 1.63/1.69 ! [X_a] : ti(fun(X_a,fun(X_a,bool)),fequal(X_a)) = fequal(X_a) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_hAPP_arg1,axiom, % 1.63/1.69 ! [X_b,X_a,B_1,B_2] : hAPP(X_b,X_a,ti(fun(X_b,X_a),B_1),B_2) = hAPP(X_b,X_a,B_1,B_2) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_hAPP_arg2,axiom, % 1.63/1.69 ! [X_b,X_a,B_1,B_2] : hAPP(X_b,X_a,B_1,ti(X_b,B_2)) = hAPP(X_b,X_a,B_1,B_2) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_hAPP_res,axiom, % 1.63/1.69 ! [X_a,X_b,B_1,B_2] : ti(X_a,hAPP(X_b,X_a,B_1,B_2)) = hAPP(X_b,X_a,B_1,B_2) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_hBOOL_arg1,hypothesis, % 1.63/1.69 ! [B_1] : % 1.63/1.69 ( hBOOL(ti(bool,B_1)) % 1.63/1.69 <=> hBOOL(B_1) ) ). % 1.63/1.69 % 1.63/1.69 fof(tsy_c_member_res,axiom, % 1.63/1.69 ! [X_b] : ti(fun(X_b,fun(fun(X_b,bool),bool)),member(X_b)) = member(X_b) ). % 1.63/1.69 % 1.63/1.69 %----Relevant facts (32) % 1.63/1.69 fof(fact_0_state__not__singleton__def,axiom, % 1.63/1.69 ( hBOOL(hoare_1883395792gleton) % 1.63/1.69 <=> ? [S,T] : ti(state,S) != ti(state,T) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_1_equal__triple__def,axiom, % 1.63/1.69 ! [X_a,X_1,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(hoare_509422987triple(X_a),bool,hAPP(hoare_509422987triple(X_a),fun(hoare_509422987triple(X_a),bool),equal_equal(hoare_509422987triple(X_a)),X_1),Y_1)) % 1.63/1.69 <=> X_1 = Y_1 ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_2_Rep__triple__inject,axiom, % 1.63/1.69 ! [X_a,X_1,Y_1] : % 1.63/1.69 ( hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),X_1) = hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),Y_1) % 1.63/1.69 <=> X_1 = Y_1 ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_3_equal,axiom, % 1.63/1.69 ! [X_a] : % 1.63/1.69 ( cl_HOL_Oequal(X_a) % 1.63/1.69 => equal_equal(X_a) = fequal(X_a) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_4_equal__refl,axiom, % 1.63/1.69 ! [X_a] : % 1.63/1.69 ( cl_HOL_Oequal(X_a) % 1.63/1.69 => ! [X] : hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),equal_equal(X_a),X),X)) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_5_equal__eq,axiom, % 1.63/1.69 ! [X_a] : % 1.63/1.69 ( cl_HOL_Oequal(X_a) % 1.63/1.69 => ! [X_1,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),equal_equal(X_a),X_1),Y_1)) % 1.63/1.69 <=> ti(X_a,X_1) = ti(X_a,Y_1) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_6_eq__equal,axiom, % 1.63/1.69 ! [X_a] : % 1.63/1.69 ( cl_HOL_Oequal(X_a) % 1.63/1.69 => fequal(X_a) = equal_equal(X_a) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_7_Rep__triple__inverse,axiom, % 1.63/1.69 ! [X_a,X_1] : hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),X_1)) = X_1 ). % 1.63/1.69 % 1.63/1.69 fof(fact_8_Rep__triple,axiom, % 1.63/1.69 ! [X_a,X_1] : hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),X_1)),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) ). % 1.63/1.69 % 1.63/1.69 fof(fact_9_Rep__triple__induct,axiom, % 1.63/1.69 ! [X_a,P,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_1),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => ( ! [X_2] : hBOOL(hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool,P,hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),X_2))) % 1.63/1.69 => hBOOL(hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool,P,Y_1)) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_10_Rep__triple__cases,axiom, % 1.63/1.69 ! [X_a,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_1),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => ~ ! [X_2] : Y_1 != hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),X_2) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_11_Abs__triple__inverse,axiom, % 1.63/1.69 ! [X_a,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_1),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => hAPP(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_2037801986triple(X_a),hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),Y_1)) = Y_1 ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_12_type__definition__triple,axiom, % 1.63/1.69 ! [X_a] : hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a)),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),hAPP(fun(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a)),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool)),type_definition(hoare_509422987triple(X_a),fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_2037801986triple(X_a)),hoare_244953527triple(X_a)),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) ). % 1.63/1.69 % 1.63/1.69 fof(fact_13_Abs__triple__inject,axiom, % 1.63/1.69 ! [X_a,Y_1,X_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),X_1),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_1),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => ( hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),X_1) = hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),Y_1) % 1.63/1.69 <=> X_1 = Y_1 ) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_14_Abs__triple__induct,axiom, % 1.63/1.69 ! [X_a,X_1,P] : % 1.63/1.69 ( ! [Y_2] : % 1.63/1.69 ( hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_2),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) % 1.63/1.69 => hBOOL(hAPP(hoare_509422987triple(X_a),bool,P,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),Y_2))) ) % 1.63/1.69 => hBOOL(hAPP(hoare_509422987triple(X_a),bool,P,X_1)) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_15_Abs__triple__cases,axiom, % 1.63/1.69 ! [X_a,X_1] : % 1.63/1.69 ~ ! [Y_2] : % 1.63/1.69 ( X_1 = hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),hoare_509422987triple(X_a),hoare_244953527triple(X_a),Y_2) % 1.63/1.69 => ~ hBOOL(hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool,hAPP(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),fun(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),bool),member(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),Y_2),hAPP(fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),fun(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool),bool),collect(fun(node(sum_sum(com,fun(X_a,fun(state,bool))),sum_sum(state,X_a)),bool)),hoare_1580379338ep_set(X_a)))) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_16_type__definition_OAbs__inject,axiom, % 1.63/1.69 ! [X_b,X_a,Y_1,X_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),X_1),A_1)) % 1.63/1.69 => ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_1),A_1)) % 1.63/1.69 => ( hAPP(X_b,X_a,Abs,X_1) = hAPP(X_b,X_a,Abs,Y_1) % 1.63/1.69 <=> ti(X_b,X_1) = ti(X_b,Y_1) ) ) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_17_type__definition_OAbs__inverse,axiom, % 1.63/1.69 ! [X_b,X_a,Y_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_1),A_1)) % 1.63/1.69 => hAPP(X_a,X_b,Rep,hAPP(X_b,X_a,Abs,Y_1)) = ti(X_b,Y_1) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_18_type__definition_ORep__inject,axiom, % 1.63/1.69 ! [X_b,X_a,X_1,Y_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( hAPP(X_a,X_b,Rep,X_1) = hAPP(X_a,X_b,Rep,Y_1) % 1.63/1.69 <=> ti(X_a,X_1) = ti(X_a,Y_1) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_19_type__definition_ORep__inverse,axiom, % 1.63/1.69 ! [X_b,X_a,X_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => hAPP(X_b,X_a,Abs,hAPP(X_a,X_b,Rep,X_1)) = ti(X_a,X_1) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_20_type__definition_ORep,axiom, % 1.63/1.69 ! [X_b,X_a,X_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),hAPP(X_a,X_b,Rep,X_1)),A_1)) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_21_induct__false__def,axiom, % 1.63/1.69 ~ hBOOL(induct_false) ). % 1.63/1.69 % 1.63/1.69 fof(fact_22_type__definition_ORep__cases,axiom, % 1.63/1.69 ! [X_b,X_a,Y_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_1),A_1)) % 1.63/1.69 => ~ ! [X_2] : ti(X_b,Y_1) != hAPP(X_a,X_b,Rep,X_2) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_23_type__definition_OAbs__cases,axiom, % 1.63/1.69 ! [X_b,X_a,X_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ~ ! [Y_2] : % 1.63/1.69 ( ti(X_a,X_1) = hAPP(X_b,X_a,Abs,Y_2) % 1.63/1.69 => ~ hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_2),A_1)) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_24_type__definition_OAbs__induct,axiom, % 1.63/1.69 ! [X_b,X_a,X_1,P,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( ! [Y_2] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_2),A_1)) % 1.63/1.69 => hBOOL(hAPP(X_a,bool,P,hAPP(X_b,X_a,Abs,Y_2))) ) % 1.63/1.69 => hBOOL(hAPP(X_a,bool,P,X_1)) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_25_type__definition_ORep__induct,axiom, % 1.63/1.69 ! [X_b,X_a,P,Y_1,Rep,Abs,A_1] : % 1.63/1.69 ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(fun(X_b,X_a),fun(fun(X_b,bool),bool),hAPP(fun(X_a,X_b),fun(fun(X_b,X_a),fun(fun(X_b,bool),bool)),type_definition(X_a,X_b),Rep),Abs),A_1)) % 1.63/1.69 => ( hBOOL(hAPP(fun(X_b,bool),bool,hAPP(X_b,fun(fun(X_b,bool),bool),member(X_b),Y_1),A_1)) % 1.63/1.69 => ( ! [X_2] : hBOOL(hAPP(X_b,bool,P,hAPP(X_a,X_b,Rep,X_2))) % 1.63/1.69 => hBOOL(hAPP(X_b,bool,P,Y_1)) ) ) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_26_induct__trueI,axiom, % 1.63/1.69 hBOOL(induct_true) ). % 1.63/1.69 % 1.63/1.69 fof(fact_27_induct__true__def,axiom, % 1.63/1.69 hBOOL(induct_true) ). % 1.63/1.69 % 1.63/1.69 fof(fact_28_induct__equal__def,axiom, % 1.63/1.69 ! [X_a,X_1,Y_1] : % 1.63/1.69 ( hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),induct_equal(X_a),X_1),Y_1)) % 1.63/1.69 <=> ti(X_a,X_1) = ti(X_a,Y_1) ) ). % 1.63/1.69 % 1.63/1.69 fof(fact_29_ext,axiom, % 1.63/1.70 ! [X_a,X_b,F,G] : % 1.63/1.70 ( ! [X_2] : hAPP(X_a,X_b,F,X_2) = hAPP(X_a,X_b,G,X_2) % 1.63/1.70 => ti(fun(X_a,X_b),F) = ti(fun(X_a,X_b),G) ) ). % 1.63/1.70 % 1.63/1.70 fof(fact_30_mem__def,axiom, % 1.63/1.70 ! [X_a,X_1,A_1] : % 1.63/1.70 ( hBOOL(hAPP(fun(X_a,bool),bool,hAPP(X_a,fun(fun(X_a,bool),bool),member(X_a),X_1),A_1)) % 1.63/1.70 <=> hBOOL(hAPP(X_a,bool,A_1,X_1)) ) ). % 1.63/1.70 % 1.63/1.70 fof(fact_31_Collect__def,axiom, % 1.63/1.70 ! [X_a,P] : hAPP(fun(X_a,bool),fun(X_a,bool),collect(X_a),P) = ti(fun(X_a,bool),P) ). % 1.63/1.70 % 1.63/1.70 %----Arities (9) % 1.63/1.70 fof(arity_sum___Enum_Oenum,axiom, % 1.63/1.70 ! [T_2,T_1_1] : % 1.63/1.70 ( ( enum(T_1_1) % 1.63/1.70 & enum(T_2) ) % 1.63/1.70 => enum(sum_sum(T_2,T_1_1)) ) ). % 1.63/1.70 % 1.63/1.70 fof(arity_HOL_Obool___Enum_Oenum,axiom, % 1.63/1.70 enum(bool) ). % 1.63/1.70 % 1.63/1.70 fof(arity_fun___Enum_Oenum,axiom, % 1.63/1.70 ! [T_2,T_1_1] : % 1.63/1.70 ( ( enum(T_1_1) % 1.63/1.70 & enum(T_2) ) % 1.63/1.70 => enum(fun(T_2,T_1_1)) ) ). % 1.63/1.70 % 1.63/1.70 fof(arity_fun___HOL_Oequal,axiom, % 1.63/1.70 ! [T_2,T_1_1] : % 1.63/1.70 ( ( cl_HOL_Oequal(T_1_1) % 1.63/1.70 & enum(T_2) ) % 1.63/1.70 => cl_HOL_Oequal(fun(T_2,T_1_1)) ) ). % 1.63/1.70 % 1.63/1.70 fof(arity_Com_Ocom___HOL_Oequal,axiom, % 1.63/1.70 cl_HOL_Oequal(com) ). % 1.63/1.70 % 1.63/1.70 fof(arity_HOL_Obool___HOL_Oequal,axiom, % 1.63/1.70 cl_HOL_Oequal(bool) ). % 1.63/1.70 % 1.63/1.70 fof(arity_Com_Ostate___HOL_Oequal,axiom, % 1.63/1.70 cl_HOL_Oequal(state) ). % 1.63/1.70 % 1.63/1.70 fof(arity_sum___HOL_Oequal,axiom, % 1.63/1.70 ! [T_2,T_1_1] : cl_HOL_Oequal(sum_sum(T_2,T_1_1)) ). % 1.63/1.70 % 1.63/1.70 fof(arity_Hoare__Mirabelle__pjuwniqynr_Otriple___HOL_Oequal,axiom, % 1.63/1.70 ! [T_1_1] : cl_HOL_Oequal(hoare_509422987triple(T_1_1)) ). % 1.63/1.70 % 1.63/1.70 %----Helper facts (3) % 1.63/1.70 fof(help_ti_idem,axiom, % 1.63/1.70 ! [T_1,A] : ti(T_1,ti(T_1,A)) = ti(T_1,A) ). % 1.63/1.70 % 1.63/1.70 fof(help_fequal_1_1_T,axiom, % 1.63/1.70 ! [X_a,X,Y] : % 1.63/1.70 ( ~ hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),fequal(X_a),X),Y)) % 1.63/1.70 | ti(X_a,X) = ti(X_a,Y) ) ). % 1.63/1.70 % 1.63/1.70 fof(help_fequal_2_1_T,axiom, % 1.63/1.70 ! [X_a,X,Y] : % 1.63/1.70 ( ti(X_a,X) != ti(X_a,Y) % 1.63/1.70 | hBOOL(hAPP(X_a,bool,hAPP(X_a,fun(X_a,bool),fequal(X_a),X),Y)) ) ). % 1.63/1.70 % 1.63/1.70 %----Conjectures (2) % 1.63/1.70 fof(conj_0,hypothesis, % 1.63/1.70 hBOOL(hoare_1883395792gleton) ). % 1.63/1.70 % 1.63/1.70 fof(conj_1,conjecture, % 1.63/1.70 ! [T] : % 1.63/1.70 ~ ! [S] : ti(state,S) = ti(state,T) ). % 1.63/1.70 % 1.63/1.70 %------------------------------------------------------------------------------ % 1.63/1.70 %------------------------------------------- % 1.63/1.70 % Proof found % 1.63/1.70 % SZS status Theorem for theBenchmark % 1.63/1.70 % SZS output start Proof % 1.63/1.70 %ClaNum:145(EqnAxiom:70) % 1.63/1.70 %VarNum:858(SingletonVarNum:189) % 1.63/1.70 %MaxLitNum:5 % 1.63/1.70 %MaxfuncDepth:4 % 1.63/1.70 %SharedTerms:28 % 1.63/1.70 %goalClause: 82 % 1.63/1.70 %singleGoalClaCount:1 % 1.63/1.70 [71]P1(a1) % 1.63/1.70 [72]P1(a2) % 1.63/1.70 [73]P1(a4) % 1.63/1.70 [75]P2(a5) % 1.63/1.70 [76]P2(a6) % 1.63/1.70 [77]P3(a1) % 1.63/1.70 [103]~P2(a27) % 1.63/1.70 [79]E(f31(a1,a27),a27) % 1.63/1.70 [80]E(f31(a1,a5),a5) % 1.63/1.70 [81]E(f31(a1,a6),a6) % 1.63/1.70 [78]P1(f24(x781)) % 1.63/1.70 [82]E(f31(a4,x821),f31(a4,a7)) % 1.63/1.70 [83]E(f31(x831,f33(x831)),f33(x831)) % 1.63/1.70 [86]E(f31(f11(x861,f11(x861,a1)),f28(x861)),f28(x861)) % 1.63/1.70 [87]E(f31(f11(x871,f11(x871,a1)),f12(x871)),f12(x871)) % 1.63/1.70 [88]E(f31(f11(f11(x881,a1),f11(x881,a1)),f3(x881)),f3(x881)) % 1.63/1.70 [89]E(f31(f11(x891,f11(f11(x891,a1),a1)),f29(x891)),f29(x891)) % 1.63/1.70 [96]E(f31(f11(f11(f30(f32(a2,f11(x961,f11(a4,a1))),f32(a4,x961)),a1),a1),f23(x961)),f23(x961)) % 1.63/1.70 [97]E(f31(f11(f24(x971),f11(f30(f32(a2,f11(x971,f11(a4,a1))),f32(a4,x971)),a1)),f26(x971)),f26(x971)) % 1.63/1.70 [98]E(f31(f11(f11(f30(f32(a2,f11(x981,f11(a4,a1))),f32(a4,x981)),a1),f24(x981)),f25(x981)),f25(x981)) % 1.63/1.70 [102]P2(f22(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),a1),a1,f22(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),f24(x1021)),f11(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),a1),a1),f22(f11(f24(x1021),f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1)),f11(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),f24(x1021)),f11(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),a1),a1)),f34(f24(x1021),f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1)),f26(x1021)),f25(x1021)),f22(f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),a1),f11(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1),a1),f3(f11(f30(f32(a2,f11(x1021,f11(a4,a1))),f32(a4,x1021)),a1)),f23(x1021)))) % 1.63/1.70 [84]P1(f32(x841,x842)) % 1.63/1.70 [85]E(f31(x851,f31(x851,x852)),f31(x851,x852)) % 1.63/1.70 [90]E(f22(f11(x901,a1),f11(x901,a1),f3(x901),x902),f31(f11(x901,a1),x902)) % 1.63/1.70 [92]E(f31(f11(f11(x921,x922),f11(f11(x922,x921),f11(f11(x922,a1),a1))),f34(x921,x922)),f34(x921,x922)) % 1.63/1.70 [95]E(f22(f11(f30(f32(a2,f11(x951,f11(a4,a1))),f32(a4,x951)),a1),f24(x951),f25(x951),f13(x951,x952)),x952) % 1.63/1.70 [99]E(f22(f11(f30(f32(a2,f11(x991,f11(a4,a1))),f32(a4,x991)),a1),f24(x991),f25(x991),f22(f24(x991),f11(f30(f32(a2,f11(x991,f11(a4,a1))),f32(a4,x991)),a1),f26(x991),x992)),x992) % 1.63/1.70 [100]P2(f22(f11(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1),f11(f11(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1)),f13(x1001,x1002)),f22(f11(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1),a1),f11(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1),a1),f3(f11(f30(f32(a2,f11(x1001,f11(a4,a1))),f32(a4,x1001)),a1)),f23(x1001)))) % 1.63/1.70 [101]P2(f22(f11(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),f11(f11(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1)),f22(f24(x1011),f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),f26(x1011),x1012)),f22(f11(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),a1),f11(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1),a1),f3(f11(f30(f32(a2,f11(x1011,f11(a4,a1))),f32(a4,x1011)),a1)),f23(x1011)))) % 1.63/1.70 [91]E(f22(x911,x912,x913,f31(x911,x914)),f22(x911,x912,x913,x914)) % 1.63/1.70 [94]E(f31(x941,f22(x942,x941,x943,x944)),f22(x942,x941,x943,x944)) % 1.63/1.70 [93]E(f22(x931,x932,f31(f11(x931,x932),x933),x934),f22(x931,x932,x933,x934)) % 1.63/1.70 [108]~E(f31(a4,a14),f31(a4,a15))+~P2(a6) % 1.63/1.70 [105]~P1(x1051)+E(f12(x1051),f8(x1051)) % 1.63/1.70 [107]~P2(x1071)+P2(f31(a1,x1071)) % 1.63/1.70 [112]P2(x1121)+~P2(f31(a1,x1121)) % 1.63/1.70 [113]~P1(x1131)+E(f31(f11(x1131,f11(x1131,a1)),f8(x1131)),f8(x1131)) % 1.63/1.70 [114]~P1(x1141)+P2(f22(x1141,a1,f22(x1141,f11(x1141,a1),f8(x1141),x1142),x1142)) % 1.63/1.70 [139]E(f22(f24(x1391),f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),f26(x1391),f17(x1391,x1392)),x1392)+~P2(f22(f11(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),f11(f11(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1)),x1392),f22(f11(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),a1),f11(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1),a1),f3(f11(f30(f32(a2,f11(x1391,f11(a4,a1))),f32(a4,x1391)),a1)),f23(x1391)))) % 1.63/1.70 [140]E(f22(f24(x1401),f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),f26(x1401),f22(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),f24(x1401),f25(x1401),x1402)),x1402)+~P2(f22(f11(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),f11(f11(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1)),x1402),f22(f11(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),a1),f11(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1),a1),f3(f11(f30(f32(a2,f11(x1401,f11(a4,a1))),f32(a4,x1401)),a1)),f23(x1401)))) % 1.63/1.70 [125]E(x1251,x1252)+~E(f22(f24(x1253),f11(f30(f32(a2,f11(x1253,f11(a4,a1))),f32(a4,x1253)),a1),f26(x1253),x1251),f22(f24(x1253),f11(f30(f32(a2,f11(x1253,f11(a4,a1))),f32(a4,x1253)),a1),f26(x1253),x1252)) % 1.63/1.70 [115]~E(f31(x1151,x1152),f31(x1151,x1153))+P2(f22(x1151,a1,f22(x1151,f11(x1151,a1),f28(x1151),x1152),x1153)) % 1.63/1.70 [116]~E(f31(x1161,x1162),f31(x1161,x1163))+P2(f22(x1161,a1,f22(x1161,f11(x1161,a1),f12(x1161),x1162),x1163)) % 1.63/1.70 [120]E(f31(x1201,x1202),f31(x1201,x1203))+~P2(f22(x1201,a1,f22(x1201,f11(x1201,a1),f28(x1201),x1202),x1203)) % 1.63/1.70 [121]E(f31(x1211,x1212),f31(x1211,x1213))+~P2(f22(x1211,a1,f22(x1211,f11(x1211,a1),f12(x1211),x1212),x1213)) % 1.63/1.70 [123]~P2(f22(x1231,a1,x1233,x1232))+P2(f22(f11(x1231,a1),a1,f22(x1231,f11(f11(x1231,a1),a1),f29(x1231),x1232),x1233)) % 1.63/1.70 [126]P2(f22(x1261,a1,x1262,x1263))+~P2(f22(f11(x1261,a1),a1,f22(x1261,f11(f11(x1261,a1),a1),f29(x1261),x1263),x1262)) % 1.63/1.70 [127]P2(f22(f24(x1271),a1,x1272,x1273))+~P2(f22(f24(x1271),a1,x1272,f22(f11(f30(f32(a2,f11(x1271,f11(a4,a1))),f32(a4,x1271)),a1),f24(x1271),f25(x1271),f16(x1271,x1273,x1272)))) % 1.63/1.70 [137]P2(f22(f24(x1371),a1,x1372,x1373))+P2(f22(f11(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1),f11(f11(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1)),f16(x1371,x1373,x1372)),f22(f11(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1),a1),f11(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1),a1),f3(f11(f30(f32(a2,f11(x1371,f11(a4,a1))),f32(a4,x1371)),a1)),f23(x1371)))) % 1.63/1.70 [118]~E(x1182,x1183)+P2(f22(f24(x1181),a1,f22(f24(x1181),f11(f24(x1181),a1),f8(f24(x1181)),x1182),x1183)) % 1.63/1.70 [124]E(x1241,x1242)+~P2(f22(f24(x1243),a1,f22(f24(x1243),f11(f24(x1243),a1),f8(f24(x1243)),x1241),x1242)) % 1.63/1.70 [119]~E(f22(x1191,x1192,x1193,f9(x1191,x1192,x1193,x1194)),f22(x1191,x1192,x1194,f9(x1191,x1192,x1193,x1194)))+E(f31(f11(x1191,x1192),x1193),f31(f11(x1191,x1192),x1194)) % 1.63/1.70 [129]E(f22(x1291,x1292,x1293,f22(x1292,x1291,x1294,x1295)),f31(x1292,x1295))+~P2(f22(f11(x1291,a1),a1,f22(f11(x1291,x1292),f11(f11(x1291,a1),a1),f22(f11(x1292,x1291),f11(f11(x1291,x1292),f11(f11(x1291,a1),a1)),f34(x1292,x1291),x1294),x1293),x1296)) % 1.63/1.70 [132]P2(f22(f11(x1321,a1),a1,f22(x1321,f11(f11(x1321,a1),a1),f29(x1321),f22(x1322,x1321,x1323,x1324)),x1325))+~P2(f22(f11(x1321,a1),a1,f22(f11(x1321,x1322),f11(f11(x1321,a1),a1),f22(f11(x1322,x1321),f11(f11(x1321,x1322),f11(f11(x1321,a1),a1)),f34(x1322,x1321),x1323),x1326),x1325)) % 1.63/1.70 [135]E(f22(x1351,x1352,x1353,f19(x1351,x1352,x1354,x1355,x1353,x1356)),f31(x1352,x1354))+~P2(f22(f11(x1351,a1),a1,f22(f11(x1351,x1352),f11(f11(x1351,a1),a1),f22(f11(x1352,x1351),f11(f11(x1351,x1352),f11(f11(x1351,a1),a1)),f34(x1352,x1351),x1355),x1353),x1356)) % 1.63/1.70 [138]P2(f22(f11(x1381,a1),a1,f22(x1381,f11(f11(x1381,a1),a1),f29(x1381),f19(x1381,x1382,x1383,x1384,x1385,x1386)),x1386))+~P2(f22(f11(x1381,a1),a1,f22(f11(x1381,x1382),f11(f11(x1381,a1),a1),f22(f11(x1382,x1381),f11(f11(x1381,x1382),f11(f11(x1381,a1),a1)),f34(x1382,x1381),x1384),x1385),x1386)) % 1.63/1.70 [109]~P1(x1092)+~P3(x1091)+P1(f11(x1091,x1092)) % 1.63/1.70 [110]~P3(x1101)+~P3(x1102)+P3(f11(x1101,x1102)) % 1.63/1.70 [111]~P3(x1111)+~P3(x1112)+P3(f32(x1111,x1112)) % 1.63/1.70 [117]~P1(x1171)+~E(f31(x1171,x1172),f31(x1171,x1173))+P2(f22(x1171,a1,f22(x1171,f11(x1171,a1),f8(x1171),x1172),x1173)) % 1.63/1.70 [122]~P1(x1221)+E(f31(x1221,x1222),f31(x1221,x1223))+~P2(f22(x1221,a1,f22(x1221,f11(x1221,a1),f8(x1221),x1222),x1223)) % 1.63/1.70 [141]~P2(f22(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1,x1412,f22(f24(x1411),f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),f26(x1411),f18(x1411,x1412,x1413))))+~P2(f22(f11(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),f11(f11(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1)),x1413),f22(f11(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1),f11(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1),f3(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1)),f23(x1411))))+P2(f22(f11(f30(f32(a2,f11(x1411,f11(a4,a1))),f32(a4,x1411)),a1),a1,x1412,x1413)) % 1.63/1.70 [131]E(f22(x1311,x1312,x1313,f22(x1312,x1311,x1314,x1315)),f31(x1312,x1315))+~P2(f22(f11(x1312,a1),a1,f22(x1312,f11(f11(x1312,a1),a1),f29(x1312),x1315),x1316))+~P2(f22(f11(x1312,a1),a1,f22(f11(x1312,x1311),f11(f11(x1312,a1),a1),f22(f11(x1311,x1312),f11(f11(x1312,x1311),f11(f11(x1312,a1),a1)),f34(x1311,x1312),x1313),x1314),x1316)) % 1.63/1.70 [136]E(f22(x1361,x1362,x1363,f20(x1362,x1361,x1364,x1363,x1365,x1366)),f31(x1362,x1364))+~P2(f22(f11(x1362,a1),a1,f22(x1362,f11(f11(x1362,a1),a1),f29(x1362),x1364),x1366))+~P2(f22(f11(x1362,a1),a1,f22(f11(x1362,x1361),f11(f11(x1362,a1),a1),f22(f11(x1361,x1362),f11(f11(x1362,x1361),f11(f11(x1362,a1),a1)),f34(x1361,x1362),x1363),x1365),x1366)) % 1.63/1.70 [128]~E(f31(x1281,x1284),f31(x1281,x1285))+E(f22(x1281,x1282,x1283,x1284),f22(x1281,x1282,x1283,x1285))+~P2(f22(f11(x1282,a1),a1,f22(f11(x1282,x1281),f11(f11(x1282,a1),a1),f22(f11(x1281,x1282),f11(f11(x1282,x1281),f11(f11(x1282,a1),a1)),f34(x1281,x1282),x1283),x1286),x1287)) % 1.63/1.70 [130]~E(f22(x1301,x1304,x1305,x1302),f22(x1301,x1304,x1305,x1303))+E(f31(x1301,x1302),f31(x1301,x1303))+~P2(f22(f11(x1304,a1),a1,f22(f11(x1304,x1301),f11(f11(x1304,a1),a1),f22(f11(x1301,x1304),f11(f11(x1304,x1301),f11(f11(x1304,a1),a1)),f34(x1301,x1304),x1305),x1306),x1307)) % 1.63/1.70 [143]P2(f22(x1431,a1,x1432,x1433))+P2(f22(f11(x1434,a1),a1,f22(x1434,f11(f11(x1434,a1),a1),f29(x1434),f21(x1434,x1431,x1433,x1432,x1435,x1436,x1437)),x1437))+~P2(f22(f11(x1434,a1),a1,f22(f11(x1434,x1431),f11(f11(x1434,a1),a1),f22(f11(x1431,x1434),f11(f11(x1434,x1431),f11(f11(x1434,a1),a1)),f34(x1431,x1434),x1435),x1436),x1437)) % 1.63/1.70 [144]P2(f22(x1441,a1,x1442,x1443))+~P2(f22(x1441,a1,x1442,f22(x1444,x1441,x1445,f21(x1444,x1441,x1443,x1442,x1446,x1445,x1447))))+~P2(f22(f11(x1444,a1),a1,f22(f11(x1444,x1441),f11(f11(x1444,a1),a1),f22(f11(x1441,x1444),f11(f11(x1444,x1441),f11(f11(x1444,a1),a1)),f34(x1441,x1444),x1446),x1445),x1447)) % 1.63/1.70 [142]E(x1421,x1422)+~E(f22(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),f24(x1423),f25(x1423),x1421),f22(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),f24(x1423),f25(x1423),x1422))+~P2(f22(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),f11(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1)),x1421),f22(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),f3(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1)),f23(x1423))))+~P2(f22(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),a1,f22(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),f11(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),a1),f29(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1)),x1422),f22(f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),f11(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1),a1),f3(f11(f30(f32(a2,f11(x1423,f11(a4,a1))),f32(a4,x1423)),a1)),f23(x1423)))) % 1.63/1.70 [145]P2(f22(x1451,a1,x1452,x1453))+~P2(f22(x1451,a1,x1452,f22(x1454,x1451,x1455,f10(x1451,x1454,x1452,x1453,x1455,x1456,x1457))))+~P2(f22(f11(x1451,a1),a1,f22(x1451,f11(f11(x1451,a1),a1),f29(x1451),x1453),x1457))+~P2(f22(f11(x1451,a1),a1,f22(f11(x1451,x1454),f11(f11(x1451,a1),a1),f22(f11(x1454,x1451),f11(f11(x1451,x1454),f11(f11(x1451,a1),a1)),f34(x1454,x1451),x1455),x1456),x1457)) % 1.63/1.70 [133]~E(f31(x1331,x1334),f31(x1331,x1335))+E(f22(x1331,x1332,x1333,x1334),f22(x1331,x1332,x1333,x1335))+~P2(f22(f11(x1331,a1),a1,f22(x1331,f11(f11(x1331,a1),a1),f29(x1331),x1334),x1336))+~P2(f22(f11(x1331,a1),a1,f22(x1331,f11(f11(x1331,a1),a1),f29(x1331),x1335),x1336))+~P2(f22(f11(x1331,a1),a1,f22(f11(x1331,x1332),f11(f11(x1331,a1),a1),f22(f11(x1332,x1331),f11(f11(x1331,x1332),f11(f11(x1331,a1),a1)),f34(x1332,x1331),x1337),x1333),x1336)) % 1.63/1.70 [134]~E(f22(x1341,x1344,x1345,x1342),f22(x1341,x1344,x1345,x1343))+E(f31(x1341,x1342),f31(x1341,x1343))+~P2(f22(f11(x1341,a1),a1,f22(x1341,f11(f11(x1341,a1),a1),f29(x1341),x1342),x1346))+~P2(f22(f11(x1341,a1),a1,f22(x1341,f11(f11(x1341,a1),a1),f29(x1341),x1343),x1346))+~P2(f22(f11(x1341,a1),a1,f22(f11(x1341,x1344),f11(f11(x1341,a1),a1),f22(f11(x1344,x1341),f11(f11(x1341,x1344),f11(f11(x1341,a1),a1)),f34(x1344,x1341),x1347),x1345),x1346)) % 1.63/1.70 %EqnAxiom % 1.63/1.70 [1]E(x11,x11) % 1.63/1.70 [2]E(x22,x21)+~E(x21,x22) % 1.63/1.70 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 1.63/1.70 [4]~E(x41,x42)+E(f24(x41),f24(x42)) % 1.63/1.70 [5]~E(x51,x52)+E(f31(x51,x53),f31(x52,x53)) % 1.63/1.70 [6]~E(x61,x62)+E(f31(x63,x61),f31(x63,x62)) % 1.63/1.70 [7]~E(x71,x72)+E(f11(x71,x73),f11(x72,x73)) % 1.63/1.70 [8]~E(x81,x82)+E(f11(x83,x81),f11(x83,x82)) % 1.63/1.70 [9]~E(x91,x92)+E(f22(x91,x93,x94,x95),f22(x92,x93,x94,x95)) % 1.63/1.70 [10]~E(x101,x102)+E(f22(x103,x101,x104,x105),f22(x103,x102,x104,x105)) % 1.63/1.70 [11]~E(x111,x112)+E(f22(x113,x114,x111,x115),f22(x113,x114,x112,x115)) % 1.63/1.70 [12]~E(x121,x122)+E(f22(x123,x124,x125,x121),f22(x123,x124,x125,x122)) % 1.63/1.70 [13]~E(x131,x132)+E(f29(x131),f29(x132)) % 1.63/1.70 [14]~E(x141,x142)+E(f30(x141,x143),f30(x142,x143)) % 1.63/1.70 [15]~E(x151,x152)+E(f30(x153,x151),f30(x153,x152)) % 1.63/1.70 [16]~E(x161,x162)+E(f33(x161),f33(x162)) % 1.63/1.70 [17]~E(x171,x172)+E(f32(x171,x173),f32(x172,x173)) % 1.63/1.70 [18]~E(x181,x182)+E(f32(x183,x181),f32(x183,x182)) % 1.63/1.70 [19]~E(x191,x192)+E(f26(x191),f26(x192)) % 1.63/1.70 [20]~E(x201,x202)+E(f34(x201,x203),f34(x202,x203)) % 1.63/1.70 [21]~E(x211,x212)+E(f34(x213,x211),f34(x213,x212)) % 1.63/1.70 [22]~E(x221,x222)+E(f25(x221),f25(x222)) % 1.63/1.70 [23]~E(x231,x232)+E(f16(x231,x233,x234),f16(x232,x233,x234)) % 1.63/1.70 [24]~E(x241,x242)+E(f16(x243,x241,x244),f16(x243,x242,x244)) % 1.63/1.70 [25]~E(x251,x252)+E(f16(x253,x254,x251),f16(x253,x254,x252)) % 1.63/1.70 [26]~E(x261,x262)+E(f9(x261,x263,x264,x265),f9(x262,x263,x264,x265)) % 1.63/1.70 [27]~E(x271,x272)+E(f9(x273,x271,x274,x275),f9(x273,x272,x274,x275)) % 1.63/1.70 [28]~E(x281,x282)+E(f9(x283,x284,x281,x285),f9(x283,x284,x282,x285)) % 1.63/1.70 [29]~E(x291,x292)+E(f9(x293,x294,x295,x291),f9(x293,x294,x295,x292)) % 1.63/1.70 [30]~E(x301,x302)+E(f23(x301),f23(x302)) % 1.63/1.70 [31]~E(x311,x312)+E(f3(x311),f3(x312)) % 1.63/1.70 [32]~E(x321,x322)+E(f28(x321),f28(x322)) % 1.63/1.70 [33]~E(x331,x332)+E(f21(x331,x333,x334,x335,x336,x337,x338),f21(x332,x333,x334,x335,x336,x337,x338)) % 1.63/1.70 [34]~E(x341,x342)+E(f21(x343,x341,x344,x345,x346,x347,x348),f21(x343,x342,x344,x345,x346,x347,x348)) % 1.63/1.70 [35]~E(x351,x352)+E(f21(x353,x354,x351,x355,x356,x357,x358),f21(x353,x354,x352,x355,x356,x357,x358)) % 1.63/1.70 [36]~E(x361,x362)+E(f21(x363,x364,x365,x361,x366,x367,x368),f21(x363,x364,x365,x362,x366,x367,x368)) % 1.63/1.70 [37]~E(x371,x372)+E(f21(x373,x374,x375,x376,x371,x377,x378),f21(x373,x374,x375,x376,x372,x377,x378)) % 1.63/1.70 [38]~E(x381,x382)+E(f21(x383,x384,x385,x386,x387,x381,x388),f21(x383,x384,x385,x386,x387,x382,x388)) % 1.63/1.70 [39]~E(x391,x392)+E(f21(x393,x394,x395,x396,x397,x398,x391),f21(x393,x394,x395,x396,x397,x398,x392)) % 1.63/1.70 [40]~E(x401,x402)+E(f12(x401),f12(x402)) % 1.63/1.70 [41]~E(x411,x412)+E(f8(x411),f8(x412)) % 1.63/1.70 [42]~E(x421,x422)+E(f13(x421,x423),f13(x422,x423)) % 1.63/1.70 [43]~E(x431,x432)+E(f13(x433,x431),f13(x433,x432)) % 1.63/1.70 [44]~E(x441,x442)+E(f19(x441,x443,x444,x445,x446,x447),f19(x442,x443,x444,x445,x446,x447)) % 1.63/1.70 [45]~E(x451,x452)+E(f19(x453,x451,x454,x455,x456,x457),f19(x453,x452,x454,x455,x456,x457)) % 1.63/1.70 [46]~E(x461,x462)+E(f19(x463,x464,x461,x465,x466,x467),f19(x463,x464,x462,x465,x466,x467)) % 1.63/1.70 [47]~E(x471,x472)+E(f19(x473,x474,x475,x471,x476,x477),f19(x473,x474,x475,x472,x476,x477)) % 1.63/1.70 [48]~E(x481,x482)+E(f19(x483,x484,x485,x486,x481,x487),f19(x483,x484,x485,x486,x482,x487)) % 1.63/1.70 [49]~E(x491,x492)+E(f19(x493,x494,x495,x496,x497,x491),f19(x493,x494,x495,x496,x497,x492)) % 1.63/1.70 [50]~E(x501,x502)+E(f18(x501,x503,x504),f18(x502,x503,x504)) % 1.63/1.70 [51]~E(x511,x512)+E(f18(x513,x511,x514),f18(x513,x512,x514)) % 1.63/1.70 [52]~E(x521,x522)+E(f18(x523,x524,x521),f18(x523,x524,x522)) % 1.63/1.70 [53]~E(x531,x532)+E(f17(x531,x533),f17(x532,x533)) % 1.63/1.70 [54]~E(x541,x542)+E(f17(x543,x541),f17(x543,x542)) % 1.63/1.70 [55]~E(x551,x552)+E(f20(x551,x553,x554,x555,x556,x557),f20(x552,x553,x554,x555,x556,x557)) % 1.63/1.70 [56]~E(x561,x562)+E(f20(x563,x561,x564,x565,x566,x567),f20(x563,x562,x564,x565,x566,x567)) % 1.63/1.70 [57]~E(x571,x572)+E(f20(x573,x574,x571,x575,x576,x577),f20(x573,x574,x572,x575,x576,x577)) % 1.63/1.70 [58]~E(x581,x582)+E(f20(x583,x584,x585,x581,x586,x587),f20(x583,x584,x585,x582,x586,x587)) % 1.63/1.70 [59]~E(x591,x592)+E(f20(x593,x594,x595,x596,x591,x597),f20(x593,x594,x595,x596,x592,x597)) % 1.63/1.70 [60]~E(x601,x602)+E(f20(x603,x604,x605,x606,x607,x601),f20(x603,x604,x605,x606,x607,x602)) % 1.63/1.70 [61]~E(x611,x612)+E(f10(x611,x613,x614,x615,x616,x617,x618),f10(x612,x613,x614,x615,x616,x617,x618)) % 1.63/1.70 [62]~E(x621,x622)+E(f10(x623,x621,x624,x625,x626,x627,x628),f10(x623,x622,x624,x625,x626,x627,x628)) % 1.63/1.70 [63]~E(x631,x632)+E(f10(x633,x634,x631,x635,x636,x637,x638),f10(x633,x634,x632,x635,x636,x637,x638)) % 1.63/1.70 [64]~E(x641,x642)+E(f10(x643,x644,x645,x641,x646,x647,x648),f10(x643,x644,x645,x642,x646,x647,x648)) % 1.63/1.70 [65]~E(x651,x652)+E(f10(x653,x654,x655,x656,x651,x657,x658),f10(x653,x654,x655,x656,x652,x657,x658)) % 1.63/1.70 [66]~E(x661,x662)+E(f10(x663,x664,x665,x666,x667,x661,x668),f10(x663,x664,x665,x666,x667,x662,x668)) % 1.63/1.70 [67]~E(x671,x672)+E(f10(x673,x674,x675,x676,x677,x678,x671),f10(x673,x674,x675,x676,x677,x678,x672)) % 1.63/1.70 [68]~P1(x681)+P1(x682)+~E(x681,x682) % 1.63/1.70 [69]~P2(x691)+P2(x692)+~E(x691,x692) % 1.63/1.70 [70]~P3(x701)+P3(x702)+~E(x701,x702) % 1.63/1.70 % 1.63/1.70 %------------------------------------------- % 1.63/1.70 cnf(146,plain, % 1.63/1.70 (P2(f22(x1461,a1,f22(x1461,f11(x1461,a1),f28(x1461),x1462),x1462))), % 1.63/1.70 inference(equality_inference,[],[115])). % 1.63/1.70 cnf(157,plain, % 1.63/1.70 (E(f31(a4,a7),f31(a4,x1571))), % 1.63/1.70 inference(scs_inference,[],[82,2])). % 1.63/1.70 cnf(158,plain, % 1.63/1.70 (E(f31(f24(x1581),x1582),x1582)), % 1.63/1.70 inference(scs_inference,[],[82,91,2,125])). % 1.63/1.70 cnf(159,plain, % 1.63/1.70 (E(f22(x1591,x1592,x1593,f31(x1591,x1594)),f22(x1591,x1592,x1593,x1594))), % 1.63/1.70 inference(rename_variables,[],[91])). % 1.63/1.70 cnf(161,plain, % 1.63/1.70 (E(f22(f24(x1611),f11(f30(f32(a2,f11(x1611,f11(a4,a1))),f32(a4,x1611)),a1),f26(x1611),f17(x1611,f13(x1611,x1612))),f13(x1611,x1612))), % 1.63/1.70 inference(scs_inference,[],[82,91,100,2,125,139])). % 1.63/1.70 cnf(163,plain, % 1.63/1.70 (E(f31(x1631,f31(x1631,f33(x1631))),f33(x1631))), % 1.63/1.70 inference(scs_inference,[],[82,83,85,91,100,2,125,139,3])). % 1.63/1.70 cnf(166,plain, % 1.63/1.70 (P2(f22(x1661,a1,f22(x1661,f11(x1661,a1),f28(x1661),f31(x1661,x1662)),x1662))), % 1.63/1.70 inference(scs_inference,[],[82,146,83,85,91,159,100,2,125,139,3,69])). % 1.63/1.70 cnf(171,plain, % 1.63/1.70 (~E(f31(a4,a14),f31(a4,a15))), % 1.63/1.70 inference(scs_inference,[],[76,108])). % 1.63/1.70 cnf(172,plain, % 1.63/1.70 (E(f33(x1721),f31(x1721,f31(x1721,f33(x1721))))), % 1.63/1.70 inference(scs_inference,[],[163,2])). % 1.63/1.70 cnf(173,plain, % 1.63/1.70 (~P2(f31(f24(x1731),a27))), % 1.63/1.70 inference(scs_inference,[],[163,158,103,2,69])). % 1.63/1.70 cnf(175,plain, % 1.63/1.70 (E(f31(a4,a7),f33(a4))), % 1.63/1.70 inference(scs_inference,[],[163,157,158,103,2,69,3])). % 1.63/1.70 cnf(185,plain, % 1.63/1.70 (E(f31(a4,x1851),f33(a4))), % 1.63/1.70 inference(scs_inference,[],[82,166,175,91,171,6,2,69,3])). % 1.63/1.70 cnf(186,plain, % 1.63/1.70 (E(f31(x1861,f31(x1861,f31(x1861,x1862))),f31(x1861,x1862))), % 1.63/1.70 inference(scs_inference,[],[82,166,175,91,171,6,2,69,3,120])). % 1.63/1.70 cnf(191,plain, % 1.63/1.70 (E(f33(a4),f31(a4,x1911))), % 1.63/1.70 inference(scs_inference,[],[185,2])). % 1.63/1.70 cnf(192,plain, % 1.63/1.70 (E(f22(f24(x1921),f11(f30(f32(a2,f11(x1921,f11(a4,a1))),f32(a4,x1921)),a1),f26(x1921),f31(f24(x1921),f31(f24(x1921),x1922))),f22(f24(x1921),f11(f30(f32(a2,f11(x1921,f11(a4,a1))),f32(a4,x1921)),a1),f26(x1921),x1922))), % 1.63/1.70 inference(scs_inference,[],[185,102,186,2,128])). % 1.63/1.70 cnf(193,plain, % 1.63/1.70 (E(f31(x1931,f31(x1931,f31(x1931,x1932))),f31(x1931,x1932))), % 1.63/1.70 inference(rename_variables,[],[186])). % 1.63/1.70 cnf(195,plain, % 1.63/1.70 (~P2(f31(f24(x1951),f31(f24(x1951),f31(f24(x1951),a27))))), % 1.63/1.70 inference(scs_inference,[],[173,185,102,186,193,2,128,69])). % 1.63/1.70 cnf(197,plain, % 1.63/1.70 (E(f31(a4,x1971),f31(a4,f31(a4,f33(a4))))), % 1.63/1.70 inference(scs_inference,[],[173,185,172,102,186,193,2,128,69,3])). % 1.63/1.70 cnf(199,plain, % 1.63/1.70 (E(f31(f24(x1991),f31(f24(x1991),x1992)),x1992)), % 1.63/1.70 inference(scs_inference,[],[173,185,172,102,186,193,2,128,69,3,125])). % 1.63/1.70 cnf(204,plain, % 1.63/1.70 (E(f31(a4,f31(a4,f33(a4))),f31(a4,x2041))), % 1.63/1.70 inference(scs_inference,[],[197,2])). % 1.63/1.70 cnf(205,plain, % 1.63/1.71 (~P2(f31(f24(x2051),f31(f24(x2051),f31(f24(x2052),f31(f24(x2052),f31(f24(x2052),a27))))))), % 1.63/1.71 inference(scs_inference,[],[195,197,199,2,69])). % 1.63/1.71 cnf(207,plain, % 1.63/1.71 (E(f22(f24(x2071),f11(f30(f32(a2,f11(x2071,f11(a4,a1))),f32(a4,x2071)),a1),f26(x2071),f31(f24(x2071),f31(f24(x2071),f31(f24(x2071),x2072)))),f22(f24(x2071),f11(f30(f32(a2,f11(x2071,f11(a4,a1))),f32(a4,x2071)),a1),f26(x2071),x2072))), % 1.63/1.71 inference(scs_inference,[],[195,192,197,91,199,2,69,3])). % 1.63/1.71 cnf(209,plain, % 1.63/1.71 (E(f31(f24(x2091),f31(f24(x2091),f31(f24(x2091),x2092))),x2092)), % 1.63/1.71 inference(scs_inference,[],[195,192,197,91,199,2,69,3,125])). % 1.63/1.71 cnf(213,plain, % 1.63/1.71 (E(f22(x2131,x2132,x2133,x2134),f22(x2131,x2132,x2133,f31(x2131,x2134)))), % 1.63/1.71 inference(scs_inference,[],[91,2])). % 1.63/1.71 cnf(214,plain, % 1.63/1.71 (~P2(f31(f24(x2141),f31(f24(x2141),f31(f24(x2141),f31(f24(x2142),f31(f24(x2142),f31(f24(x2143),f31(f24(x2143),f31(f24(x2143),a27)))))))))), % 1.63/1.71 inference(scs_inference,[],[205,91,209,2,69])). % 1.63/1.71 cnf(216,plain, % 1.63/1.71 (E(f22(f24(x2161),f11(f30(f32(a2,f11(x2161,f11(a4,a1))),f32(a4,x2161)),a1),f26(x2161),f31(f24(x2161),f31(f24(x2161),f31(f24(x2161),f31(f24(x2161),f31(f24(x2161),x2162)))))),f22(f24(x2161),f11(f30(f32(a2,f11(x2161,f11(a4,a1))),f32(a4,x2161)),a1),f26(x2161),x2162))), % 1.63/1.71 inference(scs_inference,[],[205,207,192,91,209,2,69,3])). % 1.63/1.71 cnf(219,plain, % 1.63/1.71 (E(x2191,f31(f24(x2192),x2191))), % 1.63/1.71 inference(scs_inference,[],[205,207,192,91,209,2,69,3,125])). % 1.63/1.71 cnf(222,plain, % 1.63/1.71 (P1(f31(f24(x2221),a1))), % 1.63/1.71 inference(scs_inference,[],[205,207,204,192,91,209,71,2,69,3,125,70,68])). % 1.63/1.71 cnf(224,plain, % 1.63/1.71 (E(f13(x2241,x2242),f22(f24(x2241),f11(f30(f32(a2,f11(x2241,f11(a4,a1))),f32(a4,x2241)),a1),f26(x2241),f17(x2241,f13(x2241,x2242))))), % 1.63/1.71 inference(scs_inference,[],[161,2])). % 1.63/1.71 cnf(225,plain, % 1.63/1.71 (P3(f31(f24(x2251),a1))), % 1.63/1.71 inference(scs_inference,[],[219,161,77,2,70])). % 1.63/1.71 cnf(226,plain, % 1.63/1.71 (E(x2261,f31(f24(x2262),x2261))), % 1.63/1.71 inference(rename_variables,[],[219])). % 1.63/1.71 cnf(228,plain, % 1.63/1.71 (E(x2281,f31(f24(x2282),x2281))), % 1.63/1.71 inference(rename_variables,[],[219])). % 1.63/1.71 cnf(229,plain, % 1.63/1.71 (P1(f31(f24(x2291),f31(f24(x2292),a1)))), % 1.63/1.71 inference(scs_inference,[],[166,222,219,226,228,161,77,2,70,69,68])). % 1.63/1.71 cnf(231,plain, % 1.63/1.71 (E(f22(f24(x2311),f11(f30(f32(a2,f11(x2311,f11(a4,a1))),f32(a4,x2311)),a1),f26(x2311),f31(f24(x2311),f31(f24(x2311),f31(f24(x2311),f31(f24(x2311),f31(f24(x2311),x2312)))))),f22(f24(x2311),f11(f30(f32(a2,f11(x2311,f11(a4,a1))),f32(a4,x2311)),a1),f26(x2311),f31(f24(x2311),x2312)))), % 1.63/1.71 inference(scs_inference,[],[166,213,216,222,219,226,228,161,77,2,70,69,68,3])). % 1.63/1.71 cnf(233,plain, % 1.63/1.71 (E(f22(x2331,x2332,x2333,x2334),f31(x2332,f22(x2331,x2332,x2333,x2334)))), % 1.63/1.71 inference(scs_inference,[],[94,2])). % 1.63/1.71 cnf(237,plain, % 1.63/1.71 (P3(f31(f24(x2371),f31(f24(x2372),a1)))), % 1.63/1.71 inference(scs_inference,[],[231,225,102,94,219,2,130,70])). % 1.63/1.71 cnf(238,plain, % 1.63/1.71 (E(x2381,f31(f24(x2382),x2381))), % 1.63/1.71 inference(rename_variables,[],[219])). % 1.63/1.71 cnf(239,plain, % 1.63/1.71 (~P2(f22(f11(f30(f32(a2,f11(x2391,f11(a4,a1))),f32(a4,x2391)),a1),f24(x2391),f25(x2391),f13(x2391,f31(f24(x2392),f31(f24(x2392),f31(f24(x2392),f31(f24(x2393),f31(f24(x2393),f31(f24(x2394),f31(f24(x2394),f31(f24(x2394),a27)))))))))))), % 1.63/1.71 inference(scs_inference,[],[214,231,225,102,94,95,219,2,130,70,69])). % 1.63/1.71 cnf(240,plain, % 1.63/1.71 (E(f22(f11(f30(f32(a2,f11(x2401,f11(a4,a1))),f32(a4,x2401)),a1),f24(x2401),f25(x2401),f13(x2401,x2402)),x2402)), % 1.63/1.71 inference(rename_variables,[],[95])). % 1.63/1.71 cnf(243,plain, % 1.63/1.71 (E(f22(f11(f30(f32(a2,f11(x2431,f11(a4,a1))),f32(a4,x2431)),a1),f24(x2431),f25(x2431),f13(x2431,f13(x2432,x2433))),f22(f24(x2432),f11(f30(f32(a2,f11(x2432,f11(a4,a1))),f32(a4,x2432)),a1),f26(x2432),f17(x2432,f13(x2432,x2433))))), % 1.63/1.71 inference(scs_inference,[],[214,224,231,229,225,102,94,95,240,219,238,2,130,70,69,68,3])). % 1.63/1.71 cnf(246,plain, % 1.63/1.71 (P3(f31(f24(x2461),f31(f24(x2462),f31(f24(x2463),a1))))), % 1.63/1.71 inference(scs_inference,[],[243,237,219,2,70])). % 1.63/1.71 cnf(248,plain, % 1.63/1.71 (P2(f31(a1,f22(x2481,a1,f22(x2481,f11(x2481,a1),f28(x2481),f31(x2481,x2482)),x2482)))), % 1.63/1.71 inference(scs_inference,[],[166,233,243,237,219,2,70,69])). % 1.63/1.71 cnf(257,plain, % 1.63/1.71 (~P2(f31(a1,a27))), % 1.63/1.71 inference(scs_inference,[],[246,92,79,103,219,2,70,69])). % 1.63/1.71 cnf(262,plain, % 1.63/1.71 (~P2(f22(f11(f30(f32(a2,f11(x2621,f11(a4,a1))),f32(a4,x2621)),a1),f24(x2621),f31(f11(f11(f30(f32(a2,f11(x2621,f11(a4,a1))),f32(a4,x2621)),a1),f24(x2621)),f25(x2621)),f13(x2621,f31(f24(x2622),f31(f24(x2622),f31(f24(x2622),f31(f24(x2623),f31(f24(x2623),f31(f24(x2624),f31(f24(x2624),f31(f24(x2624),a27)))))))))))), % 1.63/1.71 inference(scs_inference,[],[239,86,93,2,69])). % 1.63/1.71 cnf(269,plain, % 1.63/1.71 (~P2(f31(a1,f31(a1,f31(a1,a27))))), % 1.63/1.71 inference(scs_inference,[],[257,186,2,69])). % 1.63/1.71 cnf(311,plain, % 1.63/1.71 (E(f31(x3111,x3112),f31(x3111,f31(x3111,x3112)))), % 1.63/1.71 inference(scs_inference,[],[85,2])). % 1.63/1.71 cnf(318,plain, % 1.63/1.71 (E(f12(x3181),f31(f11(x3181,f11(x3181,a1)),f12(x3181)))), % 1.63/1.71 inference(scs_inference,[],[87,2])). % 1.63/1.71 cnf(319,plain, % 1.63/1.71 (~P2(f22(f11(f30(f32(a2,f11(x3191,f11(a4,a1))),f32(a4,x3191)),a1),f24(x3191),f31(f11(f11(f30(f32(a2,f11(x3191,f11(a4,a1))),f32(a4,x3191)),a1),f24(x3191)),f31(f11(f11(f30(f32(a2,f11(x3191,f11(a4,a1))),f32(a4,x3191)),a1),f24(x3191)),f25(x3191))),f13(x3191,f31(f24(x3192),f31(f24(x3192),f31(f24(x3192),f31(f24(x3193),f31(f24(x3193),f31(f24(x3194),f31(f24(x3194),f31(f24(x3194),a27)))))))))))), % 1.63/1.71 inference(scs_inference,[],[262,87,93,2,69])). % 1.63/1.71 cnf(321,plain, % 1.63/1.71 (E(f31(a4,x3211),f31(a4,f31(a4,a7)))), % 1.63/1.71 inference(scs_inference,[],[82,311,262,87,93,2,69,3])). % 1.63/1.71 cnf(326,plain, % 1.63/1.71 (~P2(f22(f11(f30(f32(a2,f11(x3261,f11(a4,a1))),f32(a4,x3261)),a1),f24(x3261),f31(f11(f11(f30(f32(a2,f11(x3261,f11(a4,a1))),f32(a4,x3261)),a1),f24(x3261)),f31(f11(f11(f30(f32(a2,f11(x3261,f11(a4,a1))),f32(a4,x3261)),a1),f24(x3261)),f31(f11(f11(f30(f32(a2,f11(x3261,f11(a4,a1))),f32(a4,x3261)),a1),f24(x3261)),f25(x3261)))),f13(x3261,f31(f24(x3262),f31(f24(x3262),f31(f24(x3262),f31(f24(x3263),f31(f24(x3263),f31(f24(x3264),f31(f24(x3264),f31(f24(x3264),a27)))))))))))), % 1.63/1.71 inference(scs_inference,[],[319,321,93,2,69])). % 1.63/1.71 cnf(328,plain, % 1.63/1.71 (E(f31(f24(x3281),f12(x3282)),f31(f11(x3282,f11(x3282,a1)),f12(x3282)))), % 1.63/1.71 inference(scs_inference,[],[318,319,321,158,93,2,69,3])). % 1.63/1.71 cnf(332,plain, % 1.63/1.71 (E(f31(f11(x3321,f11(x3321,a1)),f12(x3321)),f31(f24(x3322),f12(x3321)))), % 1.63/1.71 inference(scs_inference,[],[328,2])). % 1.63/1.71 cnf(335,plain, % 1.63/1.71 (E(f31(f24(x3351),f31(f24(x3351),f12(x3352))),f31(f11(x3352,f11(x3352,a1)),f12(x3352)))), % 1.63/1.71 inference(scs_inference,[],[328,326,85,93,2,69,3])). % 1.63/1.71 cnf(340,plain, % 1.63/1.71 (E(f31(f24(x3401),f31(f24(x3401),f12(x3402))),f31(f24(x3403),f12(x3402)))), % 1.63/1.71 inference(scs_inference,[],[335,332,2,3])). % 1.63/1.71 cnf(346,plain, % 1.63/1.71 (E(f22(x3461,x3462,x3463,x3464),f31(x3462,f22(x3461,x3462,x3463,f31(x3461,x3464))))), % 1.63/1.71 inference(scs_inference,[],[213,233,340,2,3])). % 1.63/1.71 cnf(352,plain, % 1.63/1.71 (E(f31(x3521,f22(x3522,x3521,x3523,f31(x3522,x3524))),f22(x3522,x3521,x3523,x3524))), % 1.63/1.71 inference(scs_inference,[],[346,2])). % 1.63/1.71 cnf(358,plain, % 1.63/1.71 (E(a27,f31(a1,a27))), % 1.63/1.71 inference(scs_inference,[],[79,2])). % 1.63/1.71 cnf(359,plain, % 1.63/1.71 (E(f22(x3591,x3592,x3593,x3594),f31(x3592,f22(x3591,x3592,x3593,f31(x3591,f31(x3591,x3594)))))), % 1.63/1.71 inference(scs_inference,[],[213,346,79,2,3])). % 1.63/1.71 cnf(362,plain, % 1.63/1.71 (P2(f31(a1,f22(x3621,a1,f22(x3621,f11(x3621,a1),f28(x3621),f31(x3621,x3622)),f31(x3621,f31(x3621,x3622)))))), % 1.63/1.71 inference(scs_inference,[],[213,166,346,352,79,2,3,70,69])). % 1.63/1.71 cnf(372,plain, % 1.63/1.71 (E(f31(x3721,f22(x3722,x3721,x3723,f31(x3722,f31(x3722,x3724)))),f22(x3722,x3721,x3723,x3724))), % 1.63/1.71 inference(scs_inference,[],[359,362,112,2])). % 1.63/1.71 cnf(373,plain, % 1.63/1.71 (P2(f22(x3731,a1,f22(x3731,f11(x3731,a1),f28(x3731),f31(x3731,f31(x3731,f31(x3731,x3732)))),x3732))), % 1.63/1.71 inference(scs_inference,[],[248,359,362,112,2,69])). % 1.63/1.71 cnf(378,plain, % 1.63/1.71 (E(f31(x3781,f31(x3781,f31(x3781,f31(x3781,f31(x3781,x3782))))),f31(x3781,f31(x3781,x3782)))), % 1.63/1.71 inference(scs_inference,[],[213,248,359,362,112,2,69,3,120])). % 1.63/1.71 cnf(384,plain, % 1.63/1.71 (E(f31(x3841,f31(x3841,f31(x3841,f31(x3841,x3842)))),f31(x3841,x3842))), % 1.63/1.71 inference(scs_inference,[],[373,120])). % 1.63/1.71 cnf(386,plain, % 1.63/1.71 (E(x3861,f22(f11(f30(f32(a2,f11(x3862,f11(a4,a1))),f32(a4,x3862)),a1),f24(x3862),f25(x3862),f13(x3862,x3861)))), % 1.63/1.71 inference(scs_inference,[],[373,95,120,2])). % 1.63/1.71 cnf(391,plain, % 1.63/1.71 (~P2(f31(a1,f31(a1,f31(a1,f31(a1,f31(a1,a27))))))), % 1.63/1.71 inference(scs_inference,[],[192,269,346,373,95,378,120,2,69,3,107])). % 1.63/1.71 cnf(402,plain, % 1.63/1.71 (E(f31(a4,x4021),f22(f11(f30(f32(a2,f11(x4022,f11(a4,a1))),f32(a4,x4022)),a1),f24(x4022),f25(x4022),f13(x4022,f31(a4,a7))))), % 1.63/1.71 inference(scs_inference,[],[82,386,384,391,107,2,3])). % 1.63/1.71 cnf(409,plain, % 1.63/1.71 (E(f31(f24(x4091),f31(f24(x4091),a27)),f31(a1,a27))), % 1.63/1.71 inference(scs_inference,[],[358,402,199,2,3])). % 1.63/1.71 cnf(415,plain, % 1.63/1.71 (E(f22(x4151,x4152,x4153,f31(x4151,f31(x4151,x4154))),f22(x4151,x4152,x4153,x4154))), % 1.63/1.71 inference(scs_inference,[],[233,372,409,2,3])). % 1.63/1.71 cnf(422,plain, % 1.63/1.71 (E(f22(x4221,x4222,x4223,x4224),f31(x4222,f22(x4221,x4222,x4223,f31(x4221,f31(x4221,f31(x4221,x4224))))))), % 1.63/1.71 inference(scs_inference,[],[213,359,415,2,3])). % 1.63/1.71 cnf(434,plain, % 1.63/1.71 (E(f31(x4341,f31(x4341,f31(x4341,f31(x4341,f31(x4341,x4342))))),f31(x4341,x4342))), % 1.63/1.71 inference(scs_inference,[],[248,358,422,209,2,69,3,120])). % 1.63/1.71 cnf(584,plain, % 1.63/1.71 ($false), % 1.63/1.71 inference(scs_inference,[],[191,185,171,434,2,3]), % 1.63/1.71 ['proof']). % 1.63/1.71 % SZS output end Proof % 1.63/1.71 % Total time :1.060000s %------------------------------------------------------------------------------