%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG173+1 : TPTP v8.2.0. Released v2.7.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n029.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 03:40:55 EDT 2024 % Result : Theorem 14.29s 14.44s % Output : CNFRefutation 14.41s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG173+1 : TPTP v8.2.0. Released v2.7.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n029.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 15:29:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.50/0.59 start to proof:theBenchmark % 14.29/14.40 %------------------------------------------- % 14.29/14.40 % File :CSE---1.7 % 14.29/14.40 % Problem :theBenchmark % 14.29/14.40 % Transform :cnf % 14.29/14.40 % Format :tptp:raw % 14.29/14.40 % Command :java -jar mcs_scs.jar %d %s % 14.29/14.40 % 14.29/14.40 % Result :Theorem 13.660000s % 14.29/14.40 % Output :CNFRefutation 13.660000s % 14.29/14.40 %------------------------------------------- % 14.29/14.40 %-------------------------------------------------------------------------- % 14.29/14.40 % File : ALG173+1 : TPTP v8.2.0. Released v2.7.0. % 14.29/14.40 % Domain : General Algebra % 14.29/14.41 % Problem : Quasigroups 5 QG4: CPROPS-PAIRWISE-EXCLUSIVE-PROBLEM-4 % 14.29/14.41 % Version : Especial. % 14.29/14.41 % English : % 14.29/14.41 % 14.29/14.41 % Refs : [Mei03] Meier (2003), Email to G.Sutcliffe % 14.29/14.41 % : [CM+04] Colton et al. (2004), Automatic Generation of Classifi % 14.29/14.41 % Source : [Mei03] % 14.29/14.41 % Names : % 14.29/14.41 % 14.29/14.41 % Status : Theorem % 14.29/14.41 % Rating : 0.05 v8.2.0, 0.04 v8.1.0, 0.00 v5.3.0, 0.18 v5.2.0, 0.25 v5.0.0, 0.00 v3.7.0, 0.14 v3.5.0, 0.11 v3.4.0, 0.08 v3.3.0, 0.00 v3.2.0, 0.11 v2.7.0 % 14.29/14.41 % Syntax : Number of formulae : 7 ( 0 unt; 0 def) % 14.29/14.41 % Number of atoms : 564 ( 564 equ) % 14.29/14.41 % Maximal formula atoms : 250 ( 80 avg) % 14.29/14.41 % Number of connectives : 693 ( 136 ~; 304 |; 253 &) % 14.29/14.41 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 14.29/14.41 % Maximal formula depth : 101 ( 36 avg) % 14.29/14.41 % Maximal term depth : 4 ( 1 avg) % 14.29/14.41 % Number of predicates : 1 ( 0 usr; 0 prp; 2-2 aty) % 14.29/14.41 % Number of functors : 6 ( 6 usr; 5 con; 0-2 aty) % 14.29/14.41 % Number of variables : 0 ( 0 !; 0 ?) % 14.29/14.41 % SPC : FOF_THM_RFO_PEQ % 14.29/14.41 % 14.29/14.41 % Comments : % 14.29/14.41 %-------------------------------------------------------------------------- % 14.29/14.41 fof(ax1,axiom, % 14.29/14.41 ( ( op(e0,e0) = e0 % 14.29/14.41 | op(e0,e0) = e1 % 14.29/14.41 | op(e0,e0) = e2 % 14.29/14.41 | op(e0,e0) = e3 % 14.29/14.41 | op(e0,e0) = e4 ) % 14.29/14.41 & ( op(e0,e1) = e0 % 14.29/14.41 | op(e0,e1) = e1 % 14.29/14.41 | op(e0,e1) = e2 % 14.29/14.41 | op(e0,e1) = e3 % 14.29/14.41 | op(e0,e1) = e4 ) % 14.29/14.41 & ( op(e0,e2) = e0 % 14.29/14.41 | op(e0,e2) = e1 % 14.29/14.41 | op(e0,e2) = e2 % 14.29/14.41 | op(e0,e2) = e3 % 14.29/14.41 | op(e0,e2) = e4 ) % 14.29/14.41 & ( op(e0,e3) = e0 % 14.29/14.41 | op(e0,e3) = e1 % 14.29/14.41 | op(e0,e3) = e2 % 14.29/14.41 | op(e0,e3) = e3 % 14.29/14.41 | op(e0,e3) = e4 ) % 14.29/14.41 & ( op(e0,e4) = e0 % 14.29/14.41 | op(e0,e4) = e1 % 14.29/14.41 | op(e0,e4) = e2 % 14.29/14.41 | op(e0,e4) = e3 % 14.29/14.41 | op(e0,e4) = e4 ) % 14.29/14.41 & ( op(e1,e0) = e0 % 14.29/14.41 | op(e1,e0) = e1 % 14.29/14.41 | op(e1,e0) = e2 % 14.29/14.41 | op(e1,e0) = e3 % 14.29/14.41 | op(e1,e0) = e4 ) % 14.29/14.41 & ( op(e1,e1) = e0 % 14.29/14.41 | op(e1,e1) = e1 % 14.29/14.41 | op(e1,e1) = e2 % 14.29/14.41 | op(e1,e1) = e3 % 14.29/14.41 | op(e1,e1) = e4 ) % 14.29/14.41 & ( op(e1,e2) = e0 % 14.29/14.41 | op(e1,e2) = e1 % 14.29/14.41 | op(e1,e2) = e2 % 14.29/14.41 | op(e1,e2) = e3 % 14.29/14.41 | op(e1,e2) = e4 ) % 14.29/14.41 & ( op(e1,e3) = e0 % 14.29/14.41 | op(e1,e3) = e1 % 14.29/14.41 | op(e1,e3) = e2 % 14.29/14.41 | op(e1,e3) = e3 % 14.29/14.41 | op(e1,e3) = e4 ) % 14.29/14.41 & ( op(e1,e4) = e0 % 14.29/14.41 | op(e1,e4) = e1 % 14.29/14.41 | op(e1,e4) = e2 % 14.29/14.41 | op(e1,e4) = e3 % 14.29/14.41 | op(e1,e4) = e4 ) % 14.29/14.41 & ( op(e2,e0) = e0 % 14.29/14.41 | op(e2,e0) = e1 % 14.29/14.41 | op(e2,e0) = e2 % 14.29/14.41 | op(e2,e0) = e3 % 14.29/14.41 | op(e2,e0) = e4 ) % 14.29/14.41 & ( op(e2,e1) = e0 % 14.29/14.41 | op(e2,e1) = e1 % 14.29/14.41 | op(e2,e1) = e2 % 14.29/14.41 | op(e2,e1) = e3 % 14.29/14.41 | op(e2,e1) = e4 ) % 14.29/14.41 & ( op(e2,e2) = e0 % 14.29/14.41 | op(e2,e2) = e1 % 14.29/14.41 | op(e2,e2) = e2 % 14.29/14.41 | op(e2,e2) = e3 % 14.29/14.41 | op(e2,e2) = e4 ) % 14.29/14.41 & ( op(e2,e3) = e0 % 14.29/14.41 | op(e2,e3) = e1 % 14.29/14.41 | op(e2,e3) = e2 % 14.29/14.41 | op(e2,e3) = e3 % 14.29/14.41 | op(e2,e3) = e4 ) % 14.29/14.41 & ( op(e2,e4) = e0 % 14.29/14.41 | op(e2,e4) = e1 % 14.29/14.41 | op(e2,e4) = e2 % 14.29/14.41 | op(e2,e4) = e3 % 14.29/14.41 | op(e2,e4) = e4 ) % 14.29/14.41 & ( op(e3,e0) = e0 % 14.29/14.41 | op(e3,e0) = e1 % 14.29/14.41 | op(e3,e0) = e2 % 14.29/14.41 | op(e3,e0) = e3 % 14.29/14.41 | op(e3,e0) = e4 ) % 14.29/14.41 & ( op(e3,e1) = e0 % 14.29/14.41 | op(e3,e1) = e1 % 14.29/14.41 | op(e3,e1) = e2 % 14.29/14.41 | op(e3,e1) = e3 % 14.29/14.41 | op(e3,e1) = e4 ) % 14.29/14.41 & ( op(e3,e2) = e0 % 14.29/14.41 | op(e3,e2) = e1 % 14.29/14.41 | op(e3,e2) = e2 % 14.29/14.41 | op(e3,e2) = e3 % 14.29/14.41 | op(e3,e2) = e4 ) % 14.29/14.41 & ( op(e3,e3) = e0 % 14.29/14.41 | op(e3,e3) = e1 % 14.29/14.41 | op(e3,e3) = e2 % 14.29/14.41 | op(e3,e3) = e3 % 14.29/14.41 | op(e3,e3) = e4 ) % 14.29/14.41 & ( op(e3,e4) = e0 % 14.29/14.41 | op(e3,e4) = e1 % 14.29/14.41 | op(e3,e4) = e2 % 14.29/14.41 | op(e3,e4) = e3 % 14.29/14.41 | op(e3,e4) = e4 ) % 14.29/14.41 & ( op(e4,e0) = e0 % 14.29/14.41 | op(e4,e0) = e1 % 14.29/14.41 | op(e4,e0) = e2 % 14.29/14.41 | op(e4,e0) = e3 % 14.29/14.41 | op(e4,e0) = e4 ) % 14.29/14.41 & ( op(e4,e1) = e0 % 14.29/14.41 | op(e4,e1) = e1 % 14.29/14.41 | op(e4,e1) = e2 % 14.29/14.41 | op(e4,e1) = e3 % 14.29/14.41 | op(e4,e1) = e4 ) % 14.29/14.41 & ( op(e4,e2) = e0 % 14.29/14.41 | op(e4,e2) = e1 % 14.29/14.41 | op(e4,e2) = e2 % 14.29/14.41 | op(e4,e2) = e3 % 14.29/14.41 | op(e4,e2) = e4 ) % 14.29/14.41 & ( op(e4,e3) = e0 % 14.29/14.41 | op(e4,e3) = e1 % 14.29/14.41 | op(e4,e3) = e2 % 14.29/14.41 | op(e4,e3) = e3 % 14.29/14.41 | op(e4,e3) = e4 ) % 14.29/14.41 & ( op(e4,e4) = e0 % 14.29/14.41 | op(e4,e4) = e1 % 14.29/14.41 | op(e4,e4) = e2 % 14.29/14.41 | op(e4,e4) = e3 % 14.29/14.41 | op(e4,e4) = e4 ) ) ). % 14.29/14.41 % 14.29/14.41 fof(ax2,axiom, % 14.29/14.41 ( ( op(e0,e0) = e0 % 14.29/14.41 | op(e0,e1) = e0 % 14.29/14.41 | op(e0,e2) = e0 % 14.29/14.41 | op(e0,e3) = e0 % 14.29/14.41 | op(e0,e4) = e0 ) % 14.29/14.41 & ( op(e0,e0) = e0 % 14.29/14.41 | op(e1,e0) = e0 % 14.29/14.41 | op(e2,e0) = e0 % 14.29/14.41 | op(e3,e0) = e0 % 14.29/14.41 | op(e4,e0) = e0 ) % 14.29/14.41 & ( op(e0,e0) = e1 % 14.29/14.41 | op(e0,e1) = e1 % 14.29/14.41 | op(e0,e2) = e1 % 14.29/14.41 | op(e0,e3) = e1 % 14.29/14.41 | op(e0,e4) = e1 ) % 14.29/14.41 & ( op(e0,e0) = e1 % 14.29/14.41 | op(e1,e0) = e1 % 14.29/14.41 | op(e2,e0) = e1 % 14.29/14.41 | op(e3,e0) = e1 % 14.29/14.41 | op(e4,e0) = e1 ) % 14.29/14.41 & ( op(e0,e0) = e2 % 14.29/14.41 | op(e0,e1) = e2 % 14.29/14.41 | op(e0,e2) = e2 % 14.29/14.41 | op(e0,e3) = e2 % 14.29/14.41 | op(e0,e4) = e2 ) % 14.29/14.41 & ( op(e0,e0) = e2 % 14.29/14.41 | op(e1,e0) = e2 % 14.29/14.41 | op(e2,e0) = e2 % 14.29/14.41 | op(e3,e0) = e2 % 14.29/14.41 | op(e4,e0) = e2 ) % 14.29/14.41 & ( op(e0,e0) = e3 % 14.29/14.41 | op(e0,e1) = e3 % 14.29/14.41 | op(e0,e2) = e3 % 14.29/14.41 | op(e0,e3) = e3 % 14.29/14.41 | op(e0,e4) = e3 ) % 14.29/14.41 & ( op(e0,e0) = e3 % 14.29/14.41 | op(e1,e0) = e3 % 14.29/14.41 | op(e2,e0) = e3 % 14.29/14.41 | op(e3,e0) = e3 % 14.29/14.41 | op(e4,e0) = e3 ) % 14.29/14.41 & ( op(e0,e0) = e4 % 14.29/14.41 | op(e0,e1) = e4 % 14.29/14.41 | op(e0,e2) = e4 % 14.29/14.41 | op(e0,e3) = e4 % 14.29/14.41 | op(e0,e4) = e4 ) % 14.29/14.41 & ( op(e0,e0) = e4 % 14.29/14.41 | op(e1,e0) = e4 % 14.29/14.41 | op(e2,e0) = e4 % 14.29/14.41 | op(e3,e0) = e4 % 14.29/14.41 | op(e4,e0) = e4 ) % 14.29/14.41 & ( op(e1,e0) = e0 % 14.29/14.41 | op(e1,e1) = e0 % 14.29/14.42 | op(e1,e2) = e0 % 14.29/14.42 | op(e1,e3) = e0 % 14.29/14.42 | op(e1,e4) = e0 ) % 14.29/14.42 & ( op(e0,e1) = e0 % 14.29/14.42 | op(e1,e1) = e0 % 14.29/14.42 | op(e2,e1) = e0 % 14.29/14.42 | op(e3,e1) = e0 % 14.29/14.42 | op(e4,e1) = e0 ) % 14.29/14.42 & ( op(e1,e0) = e1 % 14.29/14.42 | op(e1,e1) = e1 % 14.29/14.42 | op(e1,e2) = e1 % 14.29/14.42 | op(e1,e3) = e1 % 14.29/14.42 | op(e1,e4) = e1 ) % 14.29/14.42 & ( op(e0,e1) = e1 % 14.29/14.42 | op(e1,e1) = e1 % 14.29/14.42 | op(e2,e1) = e1 % 14.29/14.42 | op(e3,e1) = e1 % 14.29/14.42 | op(e4,e1) = e1 ) % 14.29/14.42 & ( op(e1,e0) = e2 % 14.29/14.42 | op(e1,e1) = e2 % 14.29/14.42 | op(e1,e2) = e2 % 14.29/14.42 | op(e1,e3) = e2 % 14.29/14.42 | op(e1,e4) = e2 ) % 14.29/14.42 & ( op(e0,e1) = e2 % 14.29/14.42 | op(e1,e1) = e2 % 14.29/14.42 | op(e2,e1) = e2 % 14.29/14.42 | op(e3,e1) = e2 % 14.29/14.42 | op(e4,e1) = e2 ) % 14.29/14.42 & ( op(e1,e0) = e3 % 14.29/14.42 | op(e1,e1) = e3 % 14.29/14.42 | op(e1,e2) = e3 % 14.29/14.42 | op(e1,e3) = e3 % 14.29/14.42 | op(e1,e4) = e3 ) % 14.29/14.42 & ( op(e0,e1) = e3 % 14.29/14.42 | op(e1,e1) = e3 % 14.29/14.42 | op(e2,e1) = e3 % 14.29/14.42 | op(e3,e1) = e3 % 14.29/14.42 | op(e4,e1) = e3 ) % 14.29/14.42 & ( op(e1,e0) = e4 % 14.29/14.42 | op(e1,e1) = e4 % 14.29/14.42 | op(e1,e2) = e4 % 14.29/14.42 | op(e1,e3) = e4 % 14.29/14.42 | op(e1,e4) = e4 ) % 14.29/14.42 & ( op(e0,e1) = e4 % 14.29/14.42 | op(e1,e1) = e4 % 14.29/14.42 | op(e2,e1) = e4 % 14.29/14.42 | op(e3,e1) = e4 % 14.29/14.42 | op(e4,e1) = e4 ) % 14.29/14.42 & ( op(e2,e0) = e0 % 14.29/14.42 | op(e2,e1) = e0 % 14.29/14.42 | op(e2,e2) = e0 % 14.29/14.42 | op(e2,e3) = e0 % 14.29/14.42 | op(e2,e4) = e0 ) % 14.29/14.42 & ( op(e0,e2) = e0 % 14.29/14.42 | op(e1,e2) = e0 % 14.29/14.42 | op(e2,e2) = e0 % 14.29/14.42 | op(e3,e2) = e0 % 14.29/14.42 | op(e4,e2) = e0 ) % 14.29/14.42 & ( op(e2,e0) = e1 % 14.29/14.42 | op(e2,e1) = e1 % 14.29/14.42 | op(e2,e2) = e1 % 14.29/14.42 | op(e2,e3) = e1 % 14.29/14.42 | op(e2,e4) = e1 ) % 14.29/14.42 & ( op(e0,e2) = e1 % 14.29/14.42 | op(e1,e2) = e1 % 14.29/14.42 | op(e2,e2) = e1 % 14.29/14.42 | op(e3,e2) = e1 % 14.29/14.42 | op(e4,e2) = e1 ) % 14.29/14.42 & ( op(e2,e0) = e2 % 14.29/14.42 | op(e2,e1) = e2 % 14.29/14.42 | op(e2,e2) = e2 % 14.29/14.42 | op(e2,e3) = e2 % 14.29/14.42 | op(e2,e4) = e2 ) % 14.29/14.42 & ( op(e0,e2) = e2 % 14.29/14.42 | op(e1,e2) = e2 % 14.29/14.42 | op(e2,e2) = e2 % 14.29/14.42 | op(e3,e2) = e2 % 14.29/14.42 | op(e4,e2) = e2 ) % 14.29/14.42 & ( op(e2,e0) = e3 % 14.29/14.42 | op(e2,e1) = e3 % 14.29/14.42 | op(e2,e2) = e3 % 14.29/14.42 | op(e2,e3) = e3 % 14.29/14.42 | op(e2,e4) = e3 ) % 14.29/14.42 & ( op(e0,e2) = e3 % 14.29/14.42 | op(e1,e2) = e3 % 14.29/14.42 | op(e2,e2) = e3 % 14.29/14.42 | op(e3,e2) = e3 % 14.29/14.42 | op(e4,e2) = e3 ) % 14.29/14.42 & ( op(e2,e0) = e4 % 14.29/14.42 | op(e2,e1) = e4 % 14.29/14.42 | op(e2,e2) = e4 % 14.29/14.42 | op(e2,e3) = e4 % 14.29/14.42 | op(e2,e4) = e4 ) % 14.29/14.42 & ( op(e0,e2) = e4 % 14.29/14.42 | op(e1,e2) = e4 % 14.29/14.42 | op(e2,e2) = e4 % 14.29/14.42 | op(e3,e2) = e4 % 14.29/14.42 | op(e4,e2) = e4 ) % 14.29/14.42 & ( op(e3,e0) = e0 % 14.29/14.42 | op(e3,e1) = e0 % 14.29/14.42 | op(e3,e2) = e0 % 14.29/14.42 | op(e3,e3) = e0 % 14.29/14.42 | op(e3,e4) = e0 ) % 14.29/14.42 & ( op(e0,e3) = e0 % 14.29/14.42 | op(e1,e3) = e0 % 14.29/14.42 | op(e2,e3) = e0 % 14.29/14.42 | op(e3,e3) = e0 % 14.29/14.42 | op(e4,e3) = e0 ) % 14.29/14.42 & ( op(e3,e0) = e1 % 14.29/14.42 | op(e3,e1) = e1 % 14.29/14.42 | op(e3,e2) = e1 % 14.29/14.42 | op(e3,e3) = e1 % 14.29/14.42 | op(e3,e4) = e1 ) % 14.29/14.42 & ( op(e0,e3) = e1 % 14.29/14.42 | op(e1,e3) = e1 % 14.29/14.42 | op(e2,e3) = e1 % 14.29/14.42 | op(e3,e3) = e1 % 14.29/14.42 | op(e4,e3) = e1 ) % 14.29/14.42 & ( op(e3,e0) = e2 % 14.29/14.42 | op(e3,e1) = e2 % 14.29/14.42 | op(e3,e2) = e2 % 14.29/14.42 | op(e3,e3) = e2 % 14.29/14.42 | op(e3,e4) = e2 ) % 14.29/14.42 & ( op(e0,e3) = e2 % 14.29/14.42 | op(e1,e3) = e2 % 14.29/14.42 | op(e2,e3) = e2 % 14.29/14.42 | op(e3,e3) = e2 % 14.29/14.42 | op(e4,e3) = e2 ) % 14.29/14.42 & ( op(e3,e0) = e3 % 14.29/14.42 | op(e3,e1) = e3 % 14.29/14.42 | op(e3,e2) = e3 % 14.29/14.42 | op(e3,e3) = e3 % 14.29/14.42 | op(e3,e4) = e3 ) % 14.29/14.42 & ( op(e0,e3) = e3 % 14.29/14.42 | op(e1,e3) = e3 % 14.29/14.42 | op(e2,e3) = e3 % 14.29/14.42 | op(e3,e3) = e3 % 14.29/14.42 | op(e4,e3) = e3 ) % 14.29/14.42 & ( op(e3,e0) = e4 % 14.29/14.42 | op(e3,e1) = e4 % 14.29/14.42 | op(e3,e2) = e4 % 14.29/14.42 | op(e3,e3) = e4 % 14.29/14.42 | op(e3,e4) = e4 ) % 14.29/14.42 & ( op(e0,e3) = e4 % 14.29/14.42 | op(e1,e3) = e4 % 14.29/14.42 | op(e2,e3) = e4 % 14.29/14.42 | op(e3,e3) = e4 % 14.29/14.42 | op(e4,e3) = e4 ) % 14.29/14.42 & ( op(e4,e0) = e0 % 14.29/14.42 | op(e4,e1) = e0 % 14.29/14.42 | op(e4,e2) = e0 % 14.29/14.42 | op(e4,e3) = e0 % 14.29/14.42 | op(e4,e4) = e0 ) % 14.29/14.42 & ( op(e0,e4) = e0 % 14.29/14.42 | op(e1,e4) = e0 % 14.29/14.42 | op(e2,e4) = e0 % 14.29/14.42 | op(e3,e4) = e0 % 14.29/14.42 | op(e4,e4) = e0 ) % 14.29/14.42 & ( op(e4,e0) = e1 % 14.29/14.42 | op(e4,e1) = e1 % 14.29/14.43 | op(e4,e2) = e1 % 14.29/14.43 | op(e4,e3) = e1 % 14.29/14.43 | op(e4,e4) = e1 ) % 14.29/14.43 & ( op(e0,e4) = e1 % 14.29/14.43 | op(e1,e4) = e1 % 14.29/14.43 | op(e2,e4) = e1 % 14.29/14.43 | op(e3,e4) = e1 % 14.29/14.43 | op(e4,e4) = e1 ) % 14.29/14.43 & ( op(e4,e0) = e2 % 14.29/14.43 | op(e4,e1) = e2 % 14.29/14.43 | op(e4,e2) = e2 % 14.29/14.43 | op(e4,e3) = e2 % 14.29/14.43 | op(e4,e4) = e2 ) % 14.29/14.43 & ( op(e0,e4) = e2 % 14.29/14.43 | op(e1,e4) = e2 % 14.29/14.43 | op(e2,e4) = e2 % 14.29/14.43 | op(e3,e4) = e2 % 14.29/14.43 | op(e4,e4) = e2 ) % 14.29/14.43 & ( op(e4,e0) = e3 % 14.29/14.43 | op(e4,e1) = e3 % 14.29/14.43 | op(e4,e2) = e3 % 14.29/14.43 | op(e4,e3) = e3 % 14.29/14.43 | op(e4,e4) = e3 ) % 14.29/14.43 & ( op(e0,e4) = e3 % 14.29/14.43 | op(e1,e4) = e3 % 14.29/14.43 | op(e2,e4) = e3 % 14.29/14.43 | op(e3,e4) = e3 % 14.29/14.43 | op(e4,e4) = e3 ) % 14.29/14.43 & ( op(e4,e0) = e4 % 14.29/14.43 | op(e4,e1) = e4 % 14.29/14.43 | op(e4,e2) = e4 % 14.29/14.43 | op(e4,e3) = e4 % 14.29/14.43 | op(e4,e4) = e4 ) % 14.29/14.43 & ( op(e0,e4) = e4 % 14.29/14.43 | op(e1,e4) = e4 % 14.29/14.43 | op(e2,e4) = e4 % 14.29/14.43 | op(e3,e4) = e4 % 14.29/14.43 | op(e4,e4) = e4 ) ) ). % 14.29/14.43 % 14.29/14.43 fof(ax3,axiom, % 14.29/14.43 ( op(op(e0,e0),op(e0,e0)) = e0 % 14.29/14.43 & op(op(e1,e0),op(e0,e1)) = e0 % 14.29/14.43 & op(op(e2,e0),op(e0,e2)) = e0 % 14.29/14.43 & op(op(e3,e0),op(e0,e3)) = e0 % 14.29/14.43 & op(op(e4,e0),op(e0,e4)) = e0 % 14.29/14.43 & op(op(e0,e1),op(e1,e0)) = e1 % 14.29/14.43 & op(op(e1,e1),op(e1,e1)) = e1 % 14.29/14.43 & op(op(e2,e1),op(e1,e2)) = e1 % 14.29/14.43 & op(op(e3,e1),op(e1,e3)) = e1 % 14.29/14.43 & op(op(e4,e1),op(e1,e4)) = e1 % 14.29/14.43 & op(op(e0,e2),op(e2,e0)) = e2 % 14.29/14.43 & op(op(e1,e2),op(e2,e1)) = e2 % 14.29/14.43 & op(op(e2,e2),op(e2,e2)) = e2 % 14.29/14.43 & op(op(e3,e2),op(e2,e3)) = e2 % 14.29/14.43 & op(op(e4,e2),op(e2,e4)) = e2 % 14.29/14.43 & op(op(e0,e3),op(e3,e0)) = e3 % 14.29/14.43 & op(op(e1,e3),op(e3,e1)) = e3 % 14.29/14.43 & op(op(e2,e3),op(e3,e2)) = e3 % 14.29/14.43 & op(op(e3,e3),op(e3,e3)) = e3 % 14.29/14.43 & op(op(e4,e3),op(e3,e4)) = e3 % 14.29/14.43 & op(op(e0,e4),op(e4,e0)) = e4 % 14.29/14.43 & op(op(e1,e4),op(e4,e1)) = e4 % 14.29/14.43 & op(op(e2,e4),op(e4,e2)) = e4 % 14.29/14.43 & op(op(e3,e4),op(e4,e3)) = e4 % 14.29/14.43 & op(op(e4,e4),op(e4,e4)) = e4 ) ). % 14.29/14.43 % 14.29/14.43 fof(ax4,axiom, % 14.29/14.43 ( op(e0,e0) != op(e1,e0) % 14.29/14.43 & op(e0,e0) != op(e2,e0) % 14.29/14.43 & op(e0,e0) != op(e3,e0) % 14.29/14.43 & op(e0,e0) != op(e4,e0) % 14.29/14.43 & op(e1,e0) != op(e2,e0) % 14.29/14.43 & op(e1,e0) != op(e3,e0) % 14.29/14.43 & op(e1,e0) != op(e4,e0) % 14.29/14.43 & op(e2,e0) != op(e3,e0) % 14.29/14.43 & op(e2,e0) != op(e4,e0) % 14.29/14.43 & op(e3,e0) != op(e4,e0) % 14.29/14.43 & op(e0,e1) != op(e1,e1) % 14.29/14.43 & op(e0,e1) != op(e2,e1) % 14.29/14.43 & op(e0,e1) != op(e3,e1) % 14.29/14.43 & op(e0,e1) != op(e4,e1) % 14.29/14.43 & op(e1,e1) != op(e2,e1) % 14.29/14.43 & op(e1,e1) != op(e3,e1) % 14.29/14.43 & op(e1,e1) != op(e4,e1) % 14.29/14.43 & op(e2,e1) != op(e3,e1) % 14.29/14.43 & op(e2,e1) != op(e4,e1) % 14.29/14.43 & op(e3,e1) != op(e4,e1) % 14.29/14.43 & op(e0,e2) != op(e1,e2) % 14.29/14.43 & op(e0,e2) != op(e2,e2) % 14.29/14.43 & op(e0,e2) != op(e3,e2) % 14.29/14.43 & op(e0,e2) != op(e4,e2) % 14.29/14.43 & op(e1,e2) != op(e2,e2) % 14.29/14.43 & op(e1,e2) != op(e3,e2) % 14.29/14.43 & op(e1,e2) != op(e4,e2) % 14.29/14.43 & op(e2,e2) != op(e3,e2) % 14.29/14.43 & op(e2,e2) != op(e4,e2) % 14.29/14.43 & op(e3,e2) != op(e4,e2) % 14.29/14.43 & op(e0,e3) != op(e1,e3) % 14.29/14.43 & op(e0,e3) != op(e2,e3) % 14.29/14.43 & op(e0,e3) != op(e3,e3) % 14.29/14.43 & op(e0,e3) != op(e4,e3) % 14.29/14.43 & op(e1,e3) != op(e2,e3) % 14.29/14.43 & op(e1,e3) != op(e3,e3) % 14.29/14.43 & op(e1,e3) != op(e4,e3) % 14.29/14.43 & op(e2,e3) != op(e3,e3) % 14.29/14.43 & op(e2,e3) != op(e4,e3) % 14.29/14.43 & op(e3,e3) != op(e4,e3) % 14.29/14.43 & op(e0,e4) != op(e1,e4) % 14.29/14.43 & op(e0,e4) != op(e2,e4) % 14.29/14.43 & op(e0,e4) != op(e3,e4) % 14.29/14.43 & op(e0,e4) != op(e4,e4) % 14.29/14.43 & op(e1,e4) != op(e2,e4) % 14.29/14.43 & op(e1,e4) != op(e3,e4) % 14.29/14.43 & op(e1,e4) != op(e4,e4) % 14.29/14.43 & op(e2,e4) != op(e3,e4) % 14.29/14.43 & op(e2,e4) != op(e4,e4) % 14.29/14.43 & op(e3,e4) != op(e4,e4) % 14.29/14.43 & op(e0,e0) != op(e0,e1) % 14.29/14.43 & op(e0,e0) != op(e0,e2) % 14.29/14.43 & op(e0,e0) != op(e0,e3) % 14.29/14.43 & op(e0,e0) != op(e0,e4) % 14.29/14.43 & op(e0,e1) != op(e0,e2) % 14.29/14.43 & op(e0,e1) != op(e0,e3) % 14.29/14.43 & op(e0,e1) != op(e0,e4) % 14.29/14.43 & op(e0,e2) != op(e0,e3) % 14.29/14.43 & op(e0,e2) != op(e0,e4) % 14.29/14.43 & op(e0,e3) != op(e0,e4) % 14.29/14.43 & op(e1,e0) != op(e1,e1) % 14.29/14.43 & op(e1,e0) != op(e1,e2) % 14.29/14.43 & op(e1,e0) != op(e1,e3) % 14.29/14.43 & op(e1,e0) != op(e1,e4) % 14.29/14.43 & op(e1,e1) != op(e1,e2) % 14.29/14.43 & op(e1,e1) != op(e1,e3) % 14.29/14.43 & op(e1,e1) != op(e1,e4) % 14.29/14.43 & op(e1,e2) != op(e1,e3) % 14.29/14.43 & op(e1,e2) != op(e1,e4) % 14.29/14.43 & op(e1,e3) != op(e1,e4) % 14.29/14.43 & op(e2,e0) != op(e2,e1) % 14.29/14.43 & op(e2,e0) != op(e2,e2) % 14.29/14.43 & op(e2,e0) != op(e2,e3) % 14.29/14.43 & op(e2,e0) != op(e2,e4) % 14.29/14.43 & op(e2,e1) != op(e2,e2) % 14.29/14.43 & op(e2,e1) != op(e2,e3) % 14.29/14.43 & op(e2,e1) != op(e2,e4) % 14.29/14.43 & op(e2,e2) != op(e2,e3) % 14.29/14.43 & op(e2,e2) != op(e2,e4) % 14.29/14.43 & op(e2,e3) != op(e2,e4) % 14.29/14.43 & op(e3,e0) != op(e3,e1) % 14.29/14.43 & op(e3,e0) != op(e3,e2) % 14.29/14.43 & op(e3,e0) != op(e3,e3) % 14.29/14.43 & op(e3,e0) != op(e3,e4) % 14.29/14.43 & op(e3,e1) != op(e3,e2) % 14.29/14.43 & op(e3,e1) != op(e3,e3) % 14.29/14.43 & op(e3,e1) != op(e3,e4) % 14.29/14.43 & op(e3,e2) != op(e3,e3) % 14.29/14.43 & op(e3,e2) != op(e3,e4) % 14.29/14.43 & op(e3,e3) != op(e3,e4) % 14.29/14.43 & op(e4,e0) != op(e4,e1) % 14.29/14.43 & op(e4,e0) != op(e4,e2) % 14.29/14.43 & op(e4,e0) != op(e4,e3) % 14.29/14.43 & op(e4,e0) != op(e4,e4) % 14.29/14.43 & op(e4,e1) != op(e4,e2) % 14.29/14.43 & op(e4,e1) != op(e4,e3) % 14.29/14.43 & op(e4,e1) != op(e4,e4) % 14.29/14.43 & op(e4,e2) != op(e4,e3) % 14.29/14.43 & op(e4,e2) != op(e4,e4) % 14.29/14.43 & op(e4,e3) != op(e4,e4) ) ). % 14.29/14.43 % 14.29/14.43 fof(ax5,axiom, % 14.29/14.43 ( e0 != e1 % 14.29/14.43 & e0 != e2 % 14.29/14.43 & e0 != e3 % 14.29/14.43 & e0 != e4 % 14.29/14.43 & e1 != e2 % 14.29/14.43 & e1 != e3 % 14.29/14.43 & e1 != e4 % 14.29/14.43 & e2 != e3 % 14.29/14.43 & e2 != e4 % 14.29/14.43 & e3 != e4 ) ). % 14.29/14.43 % 14.29/14.43 fof(ax6,axiom, % 14.29/14.43 ( e0 = op(op(e3,op(e3,e3)),op(e3,op(e3,e3))) % 14.29/14.43 & e1 = op(e3,op(e3,op(e3,e3))) % 14.29/14.43 & e2 = op(e3,e3) % 14.29/14.43 & e4 = op(e3,op(e3,e3)) ) ). % 14.29/14.43 % 14.29/14.43 fof(co1,conjecture, % 14.29/14.43 ~ ( ( ( op(e0,e0) != e0 % 14.29/14.43 & op(e0,e1) != e1 % 14.29/14.43 & op(e0,e2) != e2 % 14.29/14.43 & op(e0,e3) != e3 % 14.29/14.43 & op(e0,e4) != e4 ) % 14.29/14.43 | ( op(e1,e0) != e0 % 14.29/14.43 & op(e1,e1) != e1 % 14.29/14.43 & op(e1,e2) != e2 % 14.29/14.43 & op(e1,e3) != e3 % 14.29/14.43 & op(e1,e4) != e4 ) % 14.29/14.43 | ( op(e2,e0) != e0 % 14.29/14.43 & op(e2,e1) != e1 % 14.29/14.43 & op(e2,e2) != e2 % 14.29/14.43 & op(e2,e3) != e3 % 14.29/14.43 & op(e2,e4) != e4 ) % 14.29/14.43 | ( op(e3,e0) != e0 % 14.29/14.43 & op(e3,e1) != e1 % 14.29/14.43 & op(e3,e2) != e2 % 14.29/14.43 & op(e3,e3) != e3 % 14.29/14.43 & op(e3,e4) != e4 ) % 14.29/14.43 | ( op(e4,e0) != e0 % 14.29/14.43 & op(e4,e1) != e1 % 14.29/14.43 & op(e4,e2) != e2 % 14.29/14.43 & op(e4,e3) != e3 % 14.29/14.43 & op(e4,e4) != e4 ) ) % 14.29/14.43 & op(e0,op(e0,e0)) = e0 % 14.29/14.43 & op(e0,op(e0,e1)) = e1 % 14.29/14.43 & op(e0,op(e0,e2)) = e2 % 14.29/14.43 & op(e0,op(e0,e3)) = e3 % 14.29/14.43 & op(e0,op(e0,e4)) = e4 % 14.29/14.43 & op(e1,op(e1,e0)) = e0 % 14.29/14.43 & op(e1,op(e1,e1)) = e1 % 14.29/14.43 & op(e1,op(e1,e2)) = e2 % 14.29/14.43 & op(e1,op(e1,e3)) = e3 % 14.29/14.43 & op(e1,op(e1,e4)) = e4 % 14.29/14.43 & op(e2,op(e2,e0)) = e0 % 14.29/14.43 & op(e2,op(e2,e1)) = e1 % 14.29/14.43 & op(e2,op(e2,e2)) = e2 % 14.29/14.43 & op(e2,op(e2,e3)) = e3 % 14.29/14.43 & op(e2,op(e2,e4)) = e4 % 14.29/14.44 & op(e3,op(e3,e0)) = e0 % 14.29/14.44 & op(e3,op(e3,e1)) = e1 % 14.29/14.44 & op(e3,op(e3,e2)) = e2 % 14.29/14.44 & op(e3,op(e3,e3)) = e3 % 14.29/14.44 & op(e3,op(e3,e4)) = e4 % 14.29/14.44 & op(e4,op(e4,e0)) = e0 % 14.29/14.44 & op(e4,op(e4,e1)) = e1 % 14.29/14.44 & op(e4,op(e4,e2)) = e2 % 14.29/14.44 & op(e4,op(e4,e3)) = e3 % 14.29/14.44 & op(e4,op(e4,e4)) = e4 ) ). % 14.29/14.44 % 14.29/14.44 %-------------------------------------------------------------------------- % 14.29/14.44 %------------------------------------------- % 14.29/14.44 % Proof found % 14.29/14.44 % SZS status Theorem for theBenchmark % 14.29/14.44 % SZS output start Proof % 14.29/14.44 %ClaNum:301(EqnAxiom:7) % 14.29/14.44 %VarNum:0(SingletonVarNum:0) % 14.29/14.44 %MaxLitNum:5 % 14.29/14.44 %MaxfuncDepth:3 % 14.29/14.44 %SharedTerms:390 % 14.29/14.44 %goalClause: 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 172 173 174 175 176 % 14.29/14.44 %singleGoalClaCount:25 % 14.29/14.44 [62]~E(a4,a3) % 14.29/14.44 [63]~E(a2,a3) % 14.29/14.44 [64]~E(a2,a4) % 14.29/14.44 [65]~E(a3,a1) % 14.29/14.44 [66]~E(a4,a1) % 14.29/14.44 [67]~E(a2,a1) % 14.29/14.44 [68]~E(a3,a6) % 14.29/14.44 [69]~E(a4,a6) % 14.29/14.44 [70]~E(a2,a6) % 14.29/14.44 [71]~E(a6,a1) % 14.29/14.44 [8]E(f5(a1,a1),a2) % 14.29/14.44 [72]~E(f5(a3,a4),f5(a3,a3)) % 14.29/14.44 [73]~E(f5(a3,a2),f5(a3,a3)) % 14.29/14.44 [74]~E(f5(a3,a2),f5(a3,a4)) % 14.29/14.44 [75]~E(f5(a3,a3),f5(a3,a1)) % 14.29/14.44 [76]~E(f5(a3,a4),f5(a3,a1)) % 14.29/14.44 [77]~E(f5(a3,a2),f5(a3,a1)) % 14.29/14.44 [78]~E(f5(a3,a3),f5(a3,a6)) % 14.29/14.44 [79]~E(f5(a3,a4),f5(a3,a6)) % 14.29/14.44 [80]~E(f5(a3,a2),f5(a3,a6)) % 14.29/14.44 [81]~E(f5(a3,a6),f5(a3,a1)) % 14.29/14.44 [82]~E(f5(a4,a3),f5(a3,a3)) % 14.29/14.44 [83]~E(f5(a4,a4),f5(a3,a4)) % 14.29/14.44 [84]~E(f5(a4,a4),f5(a4,a3)) % 14.29/14.44 [85]~E(f5(a4,a2),f5(a3,a2)) % 14.29/14.44 [86]~E(f5(a4,a2),f5(a4,a3)) % 14.29/14.44 [87]~E(f5(a4,a2),f5(a4,a4)) % 14.29/14.44 [88]~E(f5(a4,a1),f5(a3,a1)) % 14.29/14.44 [89]~E(f5(a4,a3),f5(a4,a1)) % 14.29/14.44 [90]~E(f5(a4,a4),f5(a4,a1)) % 14.29/14.44 [91]~E(f5(a4,a2),f5(a4,a1)) % 14.29/14.44 [92]~E(f5(a4,a6),f5(a3,a6)) % 14.29/14.44 [93]~E(f5(a4,a3),f5(a4,a6)) % 14.29/14.44 [94]~E(f5(a4,a4),f5(a4,a6)) % 14.29/14.44 [95]~E(f5(a4,a2),f5(a4,a6)) % 14.29/14.44 [96]~E(f5(a4,a6),f5(a4,a1)) % 14.29/14.44 [97]~E(f5(a2,a3),f5(a3,a3)) % 14.29/14.44 [98]~E(f5(a2,a3),f5(a4,a3)) % 14.29/14.44 [99]~E(f5(a2,a4),f5(a3,a4)) % 14.29/14.44 [100]~E(f5(a2,a4),f5(a4,a4)) % 14.29/14.44 [101]~E(f5(a2,a4),f5(a2,a3)) % 14.29/14.44 [102]~E(f5(a2,a2),f5(a3,a2)) % 14.29/14.44 [103]~E(f5(a2,a2),f5(a4,a2)) % 14.29/14.44 [104]~E(f5(a2,a2),f5(a2,a3)) % 14.29/14.44 [105]~E(f5(a2,a2),f5(a2,a4)) % 14.29/14.44 [106]~E(f5(a2,a1),f5(a3,a1)) % 14.29/14.44 [107]~E(f5(a2,a1),f5(a4,a1)) % 14.29/14.44 [108]~E(f5(a2,a3),f5(a2,a1)) % 14.29/14.44 [109]~E(f5(a2,a4),f5(a2,a1)) % 14.29/14.44 [110]~E(f5(a2,a2),f5(a2,a1)) % 14.29/14.44 [111]~E(f5(a2,a6),f5(a3,a6)) % 14.29/14.44 [112]~E(f5(a2,a6),f5(a4,a6)) % 14.29/14.44 [113]~E(f5(a2,a3),f5(a2,a6)) % 14.29/14.44 [114]~E(f5(a2,a4),f5(a2,a6)) % 14.29/14.44 [115]~E(f5(a2,a2),f5(a2,a6)) % 14.29/14.44 [116]~E(f5(a2,a6),f5(a2,a1)) % 14.29/14.44 [117]~E(f5(a3,a3),f5(a1,a3)) % 14.29/14.44 [118]~E(f5(a4,a3),f5(a1,a3)) % 14.29/14.44 [119]~E(f5(a2,a3),f5(a1,a3)) % 14.29/14.44 [120]~E(f5(a3,a4),f5(a1,a4)) % 14.29/14.44 [121]~E(f5(a4,a4),f5(a1,a4)) % 14.29/14.44 [122]~E(f5(a2,a4),f5(a1,a4)) % 14.29/14.44 [123]~E(f5(a1,a4),f5(a1,a3)) % 14.29/14.44 [124]~E(f5(a3,a2),f5(a1,a2)) % 14.29/14.44 [125]~E(f5(a4,a2),f5(a1,a2)) % 14.29/14.44 [126]~E(f5(a2,a2),f5(a1,a2)) % 14.29/14.44 [127]~E(f5(a1,a2),f5(a1,a3)) % 14.29/14.44 [128]~E(f5(a1,a2),f5(a1,a4)) % 14.29/14.44 [129]~E(f5(a3,a1),f5(a1,a1)) % 14.29/14.44 [130]~E(f5(a4,a1),f5(a1,a1)) % 14.29/14.44 [131]~E(f5(a2,a1),f5(a1,a1)) % 14.29/14.44 [132]~E(f5(a1,a3),f5(a1,a1)) % 14.29/14.44 [133]~E(f5(a1,a4),f5(a1,a1)) % 14.29/14.44 [134]~E(f5(a1,a2),f5(a1,a1)) % 14.29/14.44 [135]~E(f5(a3,a6),f5(a1,a6)) % 14.29/14.44 [136]~E(f5(a4,a6),f5(a1,a6)) % 14.29/14.44 [137]~E(f5(a2,a6),f5(a1,a6)) % 14.29/14.44 [138]~E(f5(a1,a3),f5(a1,a6)) % 14.29/14.44 [139]~E(f5(a1,a4),f5(a1,a6)) % 14.29/14.44 [140]~E(f5(a1,a2),f5(a1,a6)) % 14.29/14.44 [141]~E(f5(a1,a6),f5(a1,a1)) % 14.29/14.44 [142]~E(f5(a3,a3),f5(a6,a3)) % 14.29/14.44 [143]~E(f5(a4,a3),f5(a6,a3)) % 14.29/14.44 [144]~E(f5(a2,a3),f5(a6,a3)) % 14.29/14.44 [145]~E(f5(a6,a3),f5(a1,a3)) % 14.29/14.44 [146]~E(f5(a3,a4),f5(a6,a4)) % 14.29/14.44 [147]~E(f5(a4,a4),f5(a6,a4)) % 14.29/14.44 [148]~E(f5(a2,a4),f5(a6,a4)) % 14.29/14.44 [149]~E(f5(a6,a4),f5(a1,a4)) % 14.29/14.44 [150]~E(f5(a6,a4),f5(a6,a3)) % 14.29/14.44 [151]~E(f5(a3,a2),f5(a6,a2)) % 14.29/14.44 [152]~E(f5(a4,a2),f5(a6,a2)) % 14.29/14.44 [153]~E(f5(a2,a2),f5(a6,a2)) % 14.29/14.44 [154]~E(f5(a6,a2),f5(a1,a2)) % 14.29/14.44 [155]~E(f5(a6,a2),f5(a6,a3)) % 14.29/14.44 [156]~E(f5(a6,a2),f5(a6,a4)) % 14.29/14.44 [157]~E(f5(a3,a1),f5(a6,a1)) % 14.29/14.44 [158]~E(f5(a4,a1),f5(a6,a1)) % 14.29/14.44 [159]~E(f5(a2,a1),f5(a6,a1)) % 14.29/14.44 [160]~E(f5(a6,a1),f5(a1,a1)) % 14.29/14.44 [161]~E(f5(a6,a3),f5(a6,a1)) % 14.29/14.44 [162]~E(f5(a6,a4),f5(a6,a1)) % 14.29/14.44 [163]~E(f5(a6,a2),f5(a6,a1)) % 14.29/14.44 [164]~E(f5(a3,a6),f5(a6,a6)) % 14.29/14.44 [165]~E(f5(a4,a6),f5(a6,a6)) % 14.29/14.44 [166]~E(f5(a2,a6),f5(a6,a6)) % 14.29/14.44 [167]~E(f5(a6,a6),f5(a1,a6)) % 14.29/14.44 [168]~E(f5(a6,a3),f5(a6,a6)) % 14.29/14.44 [169]~E(f5(a6,a4),f5(a6,a6)) % 14.29/14.44 [170]~E(f5(a6,a2),f5(a6,a6)) % 14.29/14.44 [171]~E(f5(a6,a6),f5(a6,a1)) % 14.29/14.44 [9]E(f5(a1,f5(a1,a1)),a6) % 14.29/14.44 [10]E(f5(a3,f5(a3,a3)),a3) % 14.29/14.44 [11]E(f5(a3,f5(a3,a4)),a4) % 14.29/14.44 [12]E(f5(a3,f5(a3,a2)),a2) % 14.29/14.44 [13]E(f5(a3,f5(a3,a1)),a1) % 14.29/14.44 [14]E(f5(a3,f5(a3,a6)),a6) % 14.29/14.44 [15]E(f5(a4,f5(a4,a3)),a3) % 14.29/14.44 [16]E(f5(a4,f5(a4,a4)),a4) % 14.29/14.44 [17]E(f5(a4,f5(a4,a2)),a2) % 14.29/14.44 [18]E(f5(a4,f5(a4,a1)),a1) % 14.29/14.44 [19]E(f5(a4,f5(a4,a6)),a6) % 14.29/14.44 [20]E(f5(a2,f5(a2,a3)),a3) % 14.29/14.44 [21]E(f5(a2,f5(a2,a4)),a4) % 14.29/14.44 [22]E(f5(a2,f5(a2,a2)),a2) % 14.29/14.44 [23]E(f5(a2,f5(a2,a1)),a1) % 14.29/14.44 [24]E(f5(a2,f5(a2,a6)),a6) % 14.29/14.44 [25]E(f5(a1,f5(a1,a3)),a3) % 14.29/14.44 [26]E(f5(a1,f5(a1,a4)),a4) % 14.29/14.44 [27]E(f5(a1,f5(a1,a2)),a2) % 14.29/14.44 [28]E(f5(a1,f5(a1,a1)),a1) % 14.29/14.44 [29]E(f5(a1,f5(a1,a6)),a6) % 14.29/14.44 [30]E(f5(a6,f5(a6,a3)),a3) % 14.29/14.44 [31]E(f5(a6,f5(a6,a4)),a4) % 14.29/14.44 [32]E(f5(a6,f5(a6,a2)),a2) % 14.29/14.44 [33]E(f5(a6,f5(a6,a1)),a1) % 14.29/14.44 [34]E(f5(a6,f5(a6,a6)),a6) % 14.29/14.44 [35]E(f5(f5(a3,a3),f5(a3,a3)),a3) % 14.29/14.44 [36]E(f5(f5(a3,a4),f5(a4,a3)),a4) % 14.29/14.44 [37]E(f5(f5(a3,a2),f5(a2,a3)),a2) % 14.29/14.44 [38]E(f5(f5(a3,a1),f5(a1,a3)),a1) % 14.29/14.44 [39]E(f5(f5(a3,a6),f5(a6,a3)),a6) % 14.29/14.44 [40]E(f5(f5(a4,a3),f5(a3,a4)),a3) % 14.29/14.44 [41]E(f5(f5(a4,a4),f5(a4,a4)),a4) % 14.29/14.44 [42]E(f5(f5(a4,a2),f5(a2,a4)),a2) % 14.29/14.44 [43]E(f5(f5(a4,a1),f5(a1,a4)),a1) % 14.29/14.44 [44]E(f5(f5(a4,a6),f5(a6,a4)),a6) % 14.29/14.44 [45]E(f5(f5(a2,a3),f5(a3,a2)),a3) % 14.29/14.44 [46]E(f5(f5(a2,a4),f5(a4,a2)),a4) % 14.29/14.44 [47]E(f5(f5(a2,a2),f5(a2,a2)),a2) % 14.29/14.44 [48]E(f5(f5(a2,a1),f5(a1,a2)),a1) % 14.29/14.44 [49]E(f5(f5(a2,a6),f5(a6,a2)),a6) % 14.29/14.44 [50]E(f5(f5(a1,a3),f5(a3,a1)),a3) % 14.29/14.44 [51]E(f5(f5(a1,a4),f5(a4,a1)),a4) % 14.29/14.44 [52]E(f5(f5(a1,a2),f5(a2,a1)),a2) % 14.29/14.44 [53]E(f5(f5(a1,a1),f5(a1,a1)),a1) % 14.29/14.44 [54]E(f5(f5(a1,a6),f5(a6,a1)),a6) % 14.29/14.44 [55]E(f5(f5(a6,a3),f5(a3,a6)),a3) % 14.29/14.44 [56]E(f5(f5(a6,a4),f5(a4,a6)),a4) % 14.29/14.44 [57]E(f5(f5(a6,a2),f5(a2,a6)),a2) % 14.29/14.44 [58]E(f5(f5(a6,a1),f5(a1,a6)),a1) % 14.29/14.44 [59]E(f5(f5(a6,a6),f5(a6,a6)),a6) % 14.29/14.44 [60]E(f5(a1,f5(a1,f5(a1,a1))),a4) % 14.29/14.44 [61]E(f5(f5(a1,f5(a1,a1)),f5(a1,f5(a1,a1))),a3) % 14.29/14.44 [172]P1(a5000)+~E(f5(a6,a3),a3) % 14.29/14.44 [173]P1(a5000)+~E(f5(a6,a4),a4) % 14.29/14.44 [174]P1(a5000)+~E(f5(a6,a2),a2) % 14.29/14.44 [175]P1(a5000)+~E(f5(a6,a1),a1) % 14.29/14.44 [176]P1(a5000)+~E(f5(a6,a6),a6) % 14.29/14.44 [177]~P2(a5000)+~E(f5(a3,a3),a3)+~E(f5(a4,a3),a3) % 14.29/14.44 [178]~P2(a5000)+~E(f5(a3,a3),a3)+~E(f5(a4,a4),a4) % 14.29/14.44 [179]~P2(a5000)+~E(f5(a3,a3),a3)+~E(f5(a4,a2),a2) % 14.29/14.44 [180]~P2(a5000)+~E(f5(a3,a3),a3)+~E(f5(a4,a1),a1) % 14.29/14.44 [181]~P2(a5000)+~E(f5(a3,a3),a3)+~E(f5(a4,a6),a6) % 14.29/14.44 [182]~P2(a5000)+~E(f5(a4,a3),a3)+~E(f5(a3,a4),a4) % 14.29/14.44 [183]~P2(a5000)+~E(f5(a3,a4),a4)+~E(f5(a4,a4),a4) % 14.29/14.44 [184]~P2(a5000)+~E(f5(a3,a4),a4)+~E(f5(a4,a2),a2) % 14.29/14.44 [185]~P2(a5000)+~E(f5(a3,a4),a4)+~E(f5(a4,a1),a1) % 14.29/14.44 [186]~P2(a5000)+~E(f5(a3,a4),a4)+~E(f5(a4,a6),a6) % 14.29/14.44 [187]~P2(a5000)+~E(f5(a4,a3),a3)+~E(f5(a3,a2),a2) % 14.29/14.44 [188]~P2(a5000)+~E(f5(a4,a4),a4)+~E(f5(a3,a2),a2) % 14.29/14.44 [189]~P2(a5000)+~E(f5(a3,a2),a2)+~E(f5(a4,a2),a2) % 14.29/14.44 [190]~P2(a5000)+~E(f5(a3,a2),a2)+~E(f5(a4,a1),a1) % 14.29/14.44 [191]~P2(a5000)+~E(f5(a3,a2),a2)+~E(f5(a4,a6),a6) % 14.29/14.44 [192]~P2(a5000)+~E(f5(a4,a3),a3)+~E(f5(a3,a1),a1) % 14.29/14.44 [193]~P2(a5000)+~E(f5(a4,a4),a4)+~E(f5(a3,a1),a1) % 14.29/14.44 [194]~P2(a5000)+~E(f5(a4,a2),a2)+~E(f5(a3,a1),a1) % 14.29/14.44 [195]~P2(a5000)+~E(f5(a3,a1),a1)+~E(f5(a4,a1),a1) % 14.29/14.44 [196]~P2(a5000)+~E(f5(a3,a1),a1)+~E(f5(a4,a6),a6) % 14.29/14.44 [197]~P2(a5000)+~E(f5(a4,a3),a3)+~E(f5(a3,a6),a6) % 14.29/14.44 [198]~P2(a5000)+~E(f5(a4,a4),a4)+~E(f5(a3,a6),a6) % 14.29/14.44 [199]~P2(a5000)+~E(f5(a4,a2),a2)+~E(f5(a3,a6),a6) % 14.29/14.44 [200]~P2(a5000)+~E(f5(a4,a1),a1)+~E(f5(a3,a6),a6) % 14.29/14.44 [201]~P2(a5000)+~E(f5(a3,a6),a6)+~E(f5(a4,a6),a6) % 14.29/14.44 [202]P2(a5000)+~P1(a5000)+~E(f5(a2,a3),a3)+~E(f5(a1,a3),a3) % 14.29/14.44 [203]P2(a5000)+~P1(a5000)+~E(f5(a2,a3),a3)+~E(f5(a1,a4),a4) % 14.29/14.44 [204]P2(a5000)+~P1(a5000)+~E(f5(a2,a3),a3)+~E(f5(a1,a2),a2) % 14.29/14.44 [205]P2(a5000)+~P1(a5000)+~E(f5(a1,a1),a1)+~E(f5(a2,a3),a3) % 14.29/14.44 [206]P2(a5000)+~P1(a5000)+~E(f5(a2,a3),a3)+~E(f5(a1,a6),a6) % 14.29/14.44 [207]P2(a5000)+~P1(a5000)+~E(f5(a1,a3),a3)+~E(f5(a2,a4),a4) % 14.29/14.44 [208]P2(a5000)+~P1(a5000)+~E(f5(a2,a4),a4)+~E(f5(a1,a4),a4) % 14.29/14.44 [209]P2(a5000)+~P1(a5000)+~E(f5(a2,a4),a4)+~E(f5(a1,a2),a2) % 14.29/14.44 [210]P2(a5000)+~P1(a5000)+~E(f5(a1,a1),a1)+~E(f5(a2,a4),a4) % 14.29/14.44 [211]P2(a5000)+~P1(a5000)+~E(f5(a2,a4),a4)+~E(f5(a1,a6),a6) % 14.29/14.44 [212]P2(a5000)+~P1(a5000)+~E(f5(a1,a3),a3)+~E(f5(a2,a2),a2) % 14.29/14.44 [213]P2(a5000)+~P1(a5000)+~E(f5(a1,a4),a4)+~E(f5(a2,a2),a2) % 14.29/14.44 [214]P2(a5000)+~P1(a5000)+~E(f5(a2,a2),a2)+~E(f5(a1,a2),a2) % 14.29/14.44 [215]P2(a5000)+~P1(a5000)+~E(f5(a1,a1),a1)+~E(f5(a2,a2),a2) % 14.29/14.44 [216]P2(a5000)+~P1(a5000)+~E(f5(a2,a2),a2)+~E(f5(a1,a6),a6) % 14.29/14.44 [217]P2(a5000)+~P1(a5000)+~E(f5(a1,a3),a3)+~E(f5(a2,a1),a1) % 14.29/14.44 [218]P2(a5000)+~P1(a5000)+~E(f5(a1,a4),a4)+~E(f5(a2,a1),a1) % 14.29/14.44 [219]P2(a5000)+~P1(a5000)+~E(f5(a1,a2),a2)+~E(f5(a2,a1),a1) % 14.29/14.44 [220]P2(a5000)+~P1(a5000)+~E(f5(a1,a1),a1)+~E(f5(a2,a1),a1) % 14.29/14.44 [221]P2(a5000)+~P1(a5000)+~E(f5(a2,a1),a1)+~E(f5(a1,a6),a6) % 14.29/14.44 [222]P2(a5000)+~P1(a5000)+~E(f5(a1,a3),a3)+~E(f5(a2,a6),a6) % 14.29/14.44 [223]P2(a5000)+~P1(a5000)+~E(f5(a1,a4),a4)+~E(f5(a2,a6),a6) % 14.29/14.44 [224]P2(a5000)+~P1(a5000)+~E(f5(a1,a2),a2)+~E(f5(a2,a6),a6) % 14.29/14.44 [225]P2(a5000)+~P1(a5000)+~E(f5(a1,a1),a1)+~E(f5(a2,a6),a6) % 14.29/14.44 [226]P2(a5000)+~P1(a5000)+~E(f5(a2,a6),a6)+~E(f5(a1,a6),a6) % 14.29/14.44 [227]E(f5(a3,a3),a6)+E(f5(a3,a3),a1)+E(f5(a3,a3),a2)+E(f5(a3,a3),a4)+E(f5(a3,a3),a3) % 14.29/14.44 [228]E(f5(a3,a3),a3)+E(f5(a3,a4),a3)+E(f5(a3,a2),a3)+E(f5(a3,a1),a3)+E(f5(a3,a6),a3) % 14.29/14.44 [229]E(f5(a3,a3),a3)+E(f5(a4,a3),a3)+E(f5(a2,a3),a3)+E(f5(a1,a3),a3)+E(f5(a6,a3),a3) % 14.29/14.44 [230]E(f5(a3,a3),a4)+E(f5(a3,a4),a4)+E(f5(a3,a2),a4)+E(f5(a3,a1),a4)+E(f5(a3,a6),a4) % 14.29/14.44 [231]E(f5(a3,a3),a4)+E(f5(a4,a3),a4)+E(f5(a2,a3),a4)+E(f5(a1,a3),a4)+E(f5(a6,a3),a4) % 14.29/14.44 [232]E(f5(a3,a3),a2)+E(f5(a3,a4),a2)+E(f5(a3,a2),a2)+E(f5(a3,a1),a2)+E(f5(a3,a6),a2) % 14.29/14.44 [233]E(f5(a3,a3),a2)+E(f5(a4,a3),a2)+E(f5(a2,a3),a2)+E(f5(a1,a3),a2)+E(f5(a6,a3),a2) % 14.29/14.44 [234]E(f5(a3,a3),a1)+E(f5(a3,a4),a1)+E(f5(a3,a2),a1)+E(f5(a3,a1),a1)+E(f5(a3,a6),a1) % 14.29/14.44 [235]E(f5(a3,a3),a1)+E(f5(a4,a3),a1)+E(f5(a2,a3),a1)+E(f5(a1,a3),a1)+E(f5(a6,a3),a1) % 14.29/14.45 [236]E(f5(a3,a3),a6)+E(f5(a3,a4),a6)+E(f5(a3,a2),a6)+E(f5(a3,a1),a6)+E(f5(a3,a6),a6) % 14.29/14.45 [237]E(f5(a3,a3),a6)+E(f5(a4,a3),a6)+E(f5(a2,a3),a6)+E(f5(a1,a3),a6)+E(f5(a6,a3),a6) % 14.29/14.45 [238]E(f5(a3,a4),a6)+E(f5(a3,a4),a1)+E(f5(a3,a4),a2)+E(f5(a3,a4),a4)+E(f5(a3,a4),a3) % 14.29/14.45 [239]E(f5(a3,a4),a3)+E(f5(a4,a4),a3)+E(f5(a2,a4),a3)+E(f5(a1,a4),a3)+E(f5(a6,a4),a3) % 14.29/14.45 [240]E(f5(a3,a4),a4)+E(f5(a4,a4),a4)+E(f5(a2,a4),a4)+E(f5(a1,a4),a4)+E(f5(a6,a4),a4) % 14.40/14.45 [241]E(f5(a3,a4),a2)+E(f5(a4,a4),a2)+E(f5(a2,a4),a2)+E(f5(a1,a4),a2)+E(f5(a6,a4),a2) % 14.40/14.45 [242]E(f5(a3,a4),a1)+E(f5(a4,a4),a1)+E(f5(a2,a4),a1)+E(f5(a1,a4),a1)+E(f5(a6,a4),a1) % 14.40/14.45 [243]E(f5(a3,a4),a6)+E(f5(a4,a4),a6)+E(f5(a2,a4),a6)+E(f5(a1,a4),a6)+E(f5(a6,a4),a6) % 14.40/14.45 [244]E(f5(a3,a2),a6)+E(f5(a3,a2),a1)+E(f5(a3,a2),a2)+E(f5(a3,a2),a4)+E(f5(a3,a2),a3) % 14.40/14.45 [245]E(f5(a3,a2),a3)+E(f5(a4,a2),a3)+E(f5(a2,a2),a3)+E(f5(a1,a2),a3)+E(f5(a6,a2),a3) % 14.40/14.45 [246]E(f5(a3,a2),a4)+E(f5(a4,a2),a4)+E(f5(a2,a2),a4)+E(f5(a1,a2),a4)+E(f5(a6,a2),a4) % 14.40/14.45 [247]E(f5(a3,a2),a2)+E(f5(a4,a2),a2)+E(f5(a2,a2),a2)+E(f5(a1,a2),a2)+E(f5(a6,a2),a2) % 14.40/14.45 [248]E(f5(a3,a2),a1)+E(f5(a4,a2),a1)+E(f5(a2,a2),a1)+E(f5(a1,a2),a1)+E(f5(a6,a2),a1) % 14.40/14.45 [249]E(f5(a3,a2),a6)+E(f5(a4,a2),a6)+E(f5(a2,a2),a6)+E(f5(a1,a2),a6)+E(f5(a6,a2),a6) % 14.40/14.45 [250]E(f5(a3,a1),a6)+E(f5(a3,a1),a1)+E(f5(a3,a1),a2)+E(f5(a3,a1),a4)+E(f5(a3,a1),a3) % 14.40/14.45 [251]E(f5(a1,a1),a3)+E(f5(a3,a1),a3)+E(f5(a4,a1),a3)+E(f5(a2,a1),a3)+E(f5(a6,a1),a3) % 14.40/14.45 [252]E(f5(a1,a1),a4)+E(f5(a3,a1),a4)+E(f5(a4,a1),a4)+E(f5(a2,a1),a4)+E(f5(a6,a1),a4) % 14.40/14.45 [254]E(f5(a1,a1),a1)+E(f5(a3,a1),a1)+E(f5(a4,a1),a1)+E(f5(a2,a1),a1)+E(f5(a6,a1),a1) % 14.40/14.45 [255]E(f5(a3,a1),a6)+E(f5(a1,a1),a6)+E(f5(a4,a1),a6)+E(f5(a2,a1),a6)+E(f5(a6,a1),a6) % 14.40/14.45 [256]E(f5(a3,a6),a6)+E(f5(a3,a6),a1)+E(f5(a3,a6),a2)+E(f5(a3,a6),a4)+E(f5(a3,a6),a3) % 14.40/14.45 [257]E(f5(a3,a6),a3)+E(f5(a4,a6),a3)+E(f5(a2,a6),a3)+E(f5(a1,a6),a3)+E(f5(a6,a6),a3) % 14.40/14.45 [258]E(f5(a3,a6),a4)+E(f5(a4,a6),a4)+E(f5(a2,a6),a4)+E(f5(a1,a6),a4)+E(f5(a6,a6),a4) % 14.40/14.45 [259]E(f5(a3,a6),a2)+E(f5(a4,a6),a2)+E(f5(a2,a6),a2)+E(f5(a1,a6),a2)+E(f5(a6,a6),a2) % 14.40/14.45 [260]E(f5(a3,a6),a1)+E(f5(a4,a6),a1)+E(f5(a2,a6),a1)+E(f5(a1,a6),a1)+E(f5(a6,a6),a1) % 14.40/14.45 [261]E(f5(a3,a6),a6)+E(f5(a4,a6),a6)+E(f5(a2,a6),a6)+E(f5(a1,a6),a6)+E(f5(a6,a6),a6) % 14.40/14.45 [262]E(f5(a4,a3),a6)+E(f5(a4,a3),a1)+E(f5(a4,a3),a2)+E(f5(a4,a3),a4)+E(f5(a4,a3),a3) % 14.40/14.45 [263]E(f5(a4,a3),a3)+E(f5(a4,a4),a3)+E(f5(a4,a2),a3)+E(f5(a4,a1),a3)+E(f5(a4,a6),a3) % 14.40/14.45 [264]E(f5(a4,a3),a4)+E(f5(a4,a4),a4)+E(f5(a4,a2),a4)+E(f5(a4,a1),a4)+E(f5(a4,a6),a4) % 14.40/14.45 [265]E(f5(a4,a3),a2)+E(f5(a4,a4),a2)+E(f5(a4,a2),a2)+E(f5(a4,a1),a2)+E(f5(a4,a6),a2) % 14.40/14.45 [266]E(f5(a4,a3),a1)+E(f5(a4,a4),a1)+E(f5(a4,a2),a1)+E(f5(a4,a1),a1)+E(f5(a4,a6),a1) % 14.40/14.45 [267]E(f5(a4,a3),a6)+E(f5(a4,a4),a6)+E(f5(a4,a2),a6)+E(f5(a4,a1),a6)+E(f5(a4,a6),a6) % 14.40/14.45 [268]E(f5(a4,a4),a6)+E(f5(a4,a4),a1)+E(f5(a4,a4),a2)+E(f5(a4,a4),a4)+E(f5(a4,a4),a3) % 14.40/14.45 [269]E(f5(a4,a2),a6)+E(f5(a4,a2),a1)+E(f5(a4,a2),a2)+E(f5(a4,a2),a4)+E(f5(a4,a2),a3) % 14.40/14.45 [270]E(f5(a4,a1),a6)+E(f5(a4,a1),a1)+E(f5(a4,a1),a2)+E(f5(a4,a1),a4)+E(f5(a4,a1),a3) % 14.40/14.45 [271]E(f5(a4,a6),a6)+E(f5(a4,a6),a1)+E(f5(a4,a6),a2)+E(f5(a4,a6),a4)+E(f5(a4,a6),a3) % 14.40/14.45 [272]E(f5(a2,a3),a6)+E(f5(a2,a3),a1)+E(f5(a2,a3),a2)+E(f5(a2,a3),a4)+E(f5(a2,a3),a3) % 14.40/14.45 [273]E(f5(a2,a3),a3)+E(f5(a2,a4),a3)+E(f5(a2,a2),a3)+E(f5(a2,a1),a3)+E(f5(a2,a6),a3) % 14.40/14.45 [274]E(f5(a2,a3),a4)+E(f5(a2,a4),a4)+E(f5(a2,a2),a4)+E(f5(a2,a1),a4)+E(f5(a2,a6),a4) % 14.40/14.45 [275]E(f5(a2,a3),a2)+E(f5(a2,a4),a2)+E(f5(a2,a2),a2)+E(f5(a2,a1),a2)+E(f5(a2,a6),a2) % 14.40/14.45 [276]E(f5(a2,a3),a1)+E(f5(a2,a4),a1)+E(f5(a2,a2),a1)+E(f5(a2,a1),a1)+E(f5(a2,a6),a1) % 14.40/14.45 [277]E(f5(a2,a3),a6)+E(f5(a2,a4),a6)+E(f5(a2,a2),a6)+E(f5(a2,a1),a6)+E(f5(a2,a6),a6) % 14.40/14.45 [278]E(f5(a2,a4),a6)+E(f5(a2,a4),a1)+E(f5(a2,a4),a2)+E(f5(a2,a4),a4)+E(f5(a2,a4),a3) % 14.40/14.45 [279]E(f5(a2,a2),a6)+E(f5(a2,a2),a1)+E(f5(a2,a2),a2)+E(f5(a2,a2),a4)+E(f5(a2,a2),a3) % 14.40/14.45 [280]E(f5(a2,a1),a6)+E(f5(a2,a1),a1)+E(f5(a2,a1),a2)+E(f5(a2,a1),a4)+E(f5(a2,a1),a3) % 14.40/14.45 [281]E(f5(a2,a6),a6)+E(f5(a2,a6),a1)+E(f5(a2,a6),a2)+E(f5(a2,a6),a4)+E(f5(a2,a6),a3) % 14.40/14.45 [282]E(f5(a1,a3),a6)+E(f5(a1,a3),a1)+E(f5(a1,a3),a2)+E(f5(a1,a3),a4)+E(f5(a1,a3),a3) % 14.40/14.45 [283]E(f5(a1,a1),a3)+E(f5(a1,a3),a3)+E(f5(a1,a4),a3)+E(f5(a1,a2),a3)+E(f5(a1,a6),a3) % 14.40/14.45 [284]E(f5(a1,a1),a4)+E(f5(a1,a3),a4)+E(f5(a1,a4),a4)+E(f5(a1,a2),a4)+E(f5(a1,a6),a4) % 14.40/14.45 [286]E(f5(a1,a1),a1)+E(f5(a1,a3),a1)+E(f5(a1,a4),a1)+E(f5(a1,a2),a1)+E(f5(a1,a6),a1) % 14.40/14.45 [287]E(f5(a1,a3),a6)+E(f5(a1,a1),a6)+E(f5(a1,a4),a6)+E(f5(a1,a2),a6)+E(f5(a1,a6),a6) % 14.40/14.45 [288]E(f5(a1,a4),a6)+E(f5(a1,a4),a1)+E(f5(a1,a4),a2)+E(f5(a1,a4),a4)+E(f5(a1,a4),a3) % 14.40/14.45 [289]E(f5(a1,a2),a6)+E(f5(a1,a2),a1)+E(f5(a1,a2),a2)+E(f5(a1,a2),a4)+E(f5(a1,a2),a3) % 14.40/14.45 [291]E(f5(a1,a6),a6)+E(f5(a1,a6),a1)+E(f5(a1,a6),a2)+E(f5(a1,a6),a4)+E(f5(a1,a6),a3) % 14.40/14.45 [292]E(f5(a6,a3),a6)+E(f5(a6,a3),a1)+E(f5(a6,a3),a2)+E(f5(a6,a3),a4)+E(f5(a6,a3),a3) % 14.40/14.45 [293]E(f5(a6,a3),a3)+E(f5(a6,a4),a3)+E(f5(a6,a2),a3)+E(f5(a6,a1),a3)+E(f5(a6,a6),a3) % 14.40/14.45 [294]E(f5(a6,a3),a4)+E(f5(a6,a4),a4)+E(f5(a6,a2),a4)+E(f5(a6,a1),a4)+E(f5(a6,a6),a4) % 14.40/14.45 [295]E(f5(a6,a3),a2)+E(f5(a6,a4),a2)+E(f5(a6,a2),a2)+E(f5(a6,a1),a2)+E(f5(a6,a6),a2) % 14.40/14.45 [296]E(f5(a6,a3),a1)+E(f5(a6,a4),a1)+E(f5(a6,a2),a1)+E(f5(a6,a1),a1)+E(f5(a6,a6),a1) % 14.40/14.45 [297]E(f5(a6,a3),a6)+E(f5(a6,a4),a6)+E(f5(a6,a2),a6)+E(f5(a6,a1),a6)+E(f5(a6,a6),a6) % 14.40/14.45 [298]E(f5(a6,a4),a6)+E(f5(a6,a4),a1)+E(f5(a6,a4),a2)+E(f5(a6,a4),a4)+E(f5(a6,a4),a3) % 14.40/14.45 [299]E(f5(a6,a2),a6)+E(f5(a6,a2),a1)+E(f5(a6,a2),a2)+E(f5(a6,a2),a4)+E(f5(a6,a2),a3) % 14.40/14.45 [300]E(f5(a6,a1),a6)+E(f5(a6,a1),a1)+E(f5(a6,a1),a2)+E(f5(a6,a1),a4)+E(f5(a6,a1),a3) % 14.40/14.45 [301]E(f5(a6,a6),a6)+E(f5(a6,a6),a1)+E(f5(a6,a6),a2)+E(f5(a6,a6),a4)+E(f5(a6,a6),a3) % 14.40/14.45 %EqnAxiom % 14.40/14.45 [1]E(x11,x11) % 14.40/14.45 [2]E(x22,x21)+~E(x21,x22) % 14.40/14.45 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 14.40/14.45 [4]~E(x41,x42)+E(f5(x41,x43),f5(x42,x43)) % 14.40/14.45 [5]~E(x51,x52)+E(f5(x53,x51),f5(x53,x52)) % 14.40/14.45 [6]~P1(x61)+P1(x62)+~E(x61,x62) % 14.40/14.45 [7]~P2(x71)+P2(x72)+~E(x71,x72) % 14.40/14.45 % 14.40/14.45 %------------------------------------------- % 14.40/14.45 cnf(306,plain, % 14.40/14.45 (E(a1,f5(a1,f5(a1,a1)))), % 14.40/14.45 inference(scs_inference,[],[28,2])). % 14.40/14.45 cnf(312,plain, % 14.40/14.45 (E(f5(a3,f5(a3,a1)),f5(a1,f5(a1,a1)))), % 14.40/14.45 inference(scs_inference,[],[306,11,13,2,3])). % 14.40/14.45 cnf(319,plain, % 14.40/14.45 (E(a6,f5(a3,f5(a3,a6)))), % 14.40/14.45 inference(scs_inference,[],[14,2])). % 14.40/14.45 cnf(324,plain, % 14.40/14.45 (E(f5(a4,f5(a4,a6)),f5(a3,f5(a3,a6)))), % 14.40/14.45 inference(scs_inference,[],[319,15,19,2,3])). % 14.40/14.45 cnf(327,plain, % 14.40/14.45 (E(a1,f5(a4,f5(a4,a1)))), % 14.40/14.45 inference(scs_inference,[],[18,2])). % 14.40/14.45 cnf(333,plain, % 14.40/14.45 (E(f5(a2,f5(a2,a1)),f5(a4,f5(a4,a1)))), % 14.40/14.45 inference(scs_inference,[],[327,20,23,2,3])). % 14.40/14.45 cnf(376,plain, % 14.40/14.45 (E(a1,f5(a3,f5(a3,a1)))), % 14.40/14.45 inference(scs_inference,[],[13,2])). % 14.40/14.45 cnf(381,plain, % 14.40/14.45 (E(f5(a4,f5(a4,a1)),f5(a3,f5(a3,a1)))), % 14.40/14.45 inference(scs_inference,[],[376,18,16,2,3])). % 14.40/14.45 cnf(388,plain, % 14.40/14.45 (E(a6,f5(a4,f5(a4,a6)))), % 14.40/14.45 inference(scs_inference,[],[19,2])). % 14.40/14.45 cnf(392,plain, % 14.40/14.45 (E(a1,f5(a2,f5(a2,a1)))), % 14.40/14.45 inference(scs_inference,[],[23,2])). % 14.40/14.45 cnf(393,plain, % 14.40/14.45 (E(f5(a2,f5(a2,a6)),f5(a4,f5(a4,a6)))), % 14.40/14.45 inference(scs_inference,[],[388,24,23,2,3])). % 14.40/14.45 cnf(397,plain, % 14.40/14.45 (E(f5(a6,f5(a6,a1)),f5(a2,f5(a2,a1)))), % 14.40/14.45 inference(scs_inference,[],[392,33,26,2,3])). % 14.40/14.45 cnf(408,plain, % 14.40/14.45 (E(f5(a1,f5(a1,a1)),f5(a3,f5(a3,a1)))), % 14.40/14.45 inference(scs_inference,[],[312,2])). % 14.40/14.45 cnf(424,plain, % 14.40/14.45 (E(f5(a3,f5(a3,a6)),f5(a4,f5(a4,a6)))), % 14.40/14.45 inference(scs_inference,[],[324,2])). % 14.40/14.45 cnf(433,plain, % 14.40/14.45 (E(f5(a4,f5(a4,a1)),f5(a2,f5(a2,a1)))), % 14.40/14.45 inference(scs_inference,[],[333,2])). % 14.40/14.45 cnf(473,plain, % 14.40/14.45 (E(f5(a3,f5(a3,a1)),f5(a4,f5(a4,a1)))), % 14.41/14.45 inference(scs_inference,[],[381,2])). % 14.41/14.45 cnf(486,plain, % 14.41/14.45 (E(f5(a4,f5(a4,a6)),f5(a2,f5(a2,a6)))), % 14.41/14.45 inference(scs_inference,[],[393,2])). % 14.41/14.45 cnf(491,plain, % 14.41/14.45 (E(f5(a3,f5(a3,a6)),f5(a2,f5(a2,a6)))), % 14.41/14.45 inference(scs_inference,[],[486,424,397,2,3])). % 14.41/14.45 cnf(516,plain, % 14.41/14.45 (~E(a6,f5(a2,f5(a2,a1)))), % 14.41/14.45 inference(scs_inference,[],[23,491,71,2,3])). % 14.41/14.45 cnf(737,plain, % 14.41/14.45 (E(a6,f5(a1,f5(a1,a1)))), % 14.41/14.45 inference(scs_inference,[],[9,2])). % 14.41/14.45 cnf(803,plain, % 14.41/14.45 (~E(a6,f5(a4,f5(a4,a1)))), % 14.41/14.45 inference(scs_inference,[],[433,516,3])). % 14.41/14.45 cnf(810,plain, % 14.41/14.45 (~E(a6,f5(a3,f5(a3,a1)))), % 14.41/14.45 inference(scs_inference,[],[473,803,3])). % 14.41/14.45 cnf(985,plain, % 14.41/14.45 ($false), % 14.41/14.45 inference(scs_inference,[],[737,408,810,3]), % 14.41/14.45 ['proof']). % 14.41/14.45 % SZS output end Proof % 14.41/14.45 % Total time :13.660000s %------------------------------------------------------------------------------