%------------------------------------------------------------------------------ % File : Nitpick---2016 % Problem : SWV595-1 : TPTP v6.4.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_nitpick %d %s % Computer : n079.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 32218.75MB % OS : Linux 3.10.0-327.36.3.el7.x86_64 % CPULimit : 300s % DateTime : Wed Jan 18 16:48:28 EST 2017 % Result : Satisfiable 42.00s % Output : FiniteModel 42.00s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.04 % Problem : SWV595-1 : TPTP v6.4.0. Released v4.1.0. % 0.00/0.04 % Command : isabelle tptp_nitpick %d %s % 0.02/0.24 % Computer : n079.star.cs.uiowa.edu % 0.02/0.24 % Model : x86_64 x86_64 % 0.02/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.02/0.24 % Memory : 32218.75MB % 0.02/0.24 % OS : Linux 3.10.0-327.36.3.el7.x86_64 % 0.02/0.24 % CPULimit : 300 % 0.02/0.24 % DateTime : Mon Jan 16 09:58:04 CST 2017 % 0.02/0.24 % CPUTime : % 42.00/21.28 Nitpicking formula... % 42.00/21.28 Timestamp: 09:58:13 % 42.00/21.28 Using SAT solver "Lingeling_JNI" The following solvers are configured: % 42.00/21.28 "Lingeling_JNI", "CryptoMiniSat_JNI", "MiniSat_JNI", "SAT4J", "SAT4J_Light" % 42.00/21.28 Batch 1 of 20: Trying 5 scopes: % 42.00/21.28 card TPTP_Interpret.ind = 1 % 42.00/21.28 card TPTP_Interpret.ind = 2 % 42.00/21.28 card TPTP_Interpret.ind = 3 % 42.00/21.28 card TPTP_Interpret.ind = 4 % 42.00/21.28 card TPTP_Interpret.ind = 5 % 42.00/21.28 % SZS status Satisfiable % SZS output start FiniteModel % 42.00/21.28 Nitpick found a model for card TPTP_Interpret.ind = 3: % 42.00/21.28 % 42.00/21.28 Constants: % 42.00/21.28 bnd_c_Divides_Odiv__class_Odiv = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1))) % 42.00/21.28 bnd_c_Fun_Oid = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i2, i2 := i2, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_HOL_Oabs__class_Oabs = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_HOL_Oinverse__class_Odivide = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i2), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3))) % 42.00/21.28 bnd_c_HOL_Oinverse__class_Oinverse = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_HOL_Oone__class_Oone = % 42.00/21.28 (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1) % 42.00/21.28 bnd_c_HOL_Osgn__class_Osgn = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_HOL_Otimes__class_Otimes = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3))) % 42.00/21.28 bnd_c_HOL_Ouminus__class_Ouminus = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i2), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_HOL_Ozero__class_Ozero = % 42.00/21.28 (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3) % 42.00/21.28 bnd_c_Int_Oiszero = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True)) % 42.00/21.28 bnd_c_Log_Opowr = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1)) % 42.00/21.28 bnd_c_NthRoot_Osqrt = (\<lambda>x. _)(i1 := i1, i2 := i2, i3 := i3) % 42.00/21.28 bnd_c_Power_Opower__class_Opower = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1))) % 42.00/21.28 bnd_c_RealVector_Onorm__class_Onorm = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_RealVector_Oof__real = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)) % 42.00/21.28 bnd_c_RealVector_OscaleR__class_OscaleR = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i2), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i1), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i3))) % 42.00/21.28 bnd_c_Ring__and__Field_Odvd__class_Odvd = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True))) % 42.00/21.28 bnd_c_Transcendental_Ocos = % 42.00/21.28 (\<lambda>x. _)(i1 := i1, i2 := i1, i3 := i1) % 42.00/21.28 bnd_c_Transcendental_Opi = i1 % 42.00/21.28 bnd_c_Transcendental_Osin = % 42.00/21.28 (\<lambda>x. _)(i1 := i3, i2 := i3, i3 := i3) % 42.00/21.28 bnd_c_lessequals = % 42.00/21.28 (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False)), % 42.00/21.28 i2 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True)), % 42.00/21.28 i3 := (\<lambda>x. _) % 42.00/21.28 (i1 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True), % 42.00/21.28 i2 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := False), % 42.00/21.28 i3 := (\<lambda>x. _)(i1 := False, i2 := False, i3 := True))) % 42.00/21.28 bnd_class_Divides_Oring__div = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False) % 42.00/21.28 bnd_class_Divides_Osemiring__div = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False) % 42.00/21.28 bnd_class_Int_Onumber__ring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Lattices_Oboolean__algebra = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False) % 42.00/21.28 bnd_class_OrderedGroup_Oab__semigroup__idem__mult = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := False) % 42.00/21.28 bnd_class_OrderedGroup_Oab__semigroup__mult = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Ocomm__monoid__mult = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Ogroup__add = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Olordered__ab__group__add = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Omonoid__mult = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Oordered__ab__group__add = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Opordered__ab__group__add = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_OrderedGroup_Opordered__ab__group__add__abs = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Orderings_Olinorder = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Orderings_Oorder = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Orderings_Opreorder = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Power_Opower = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__algebra = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__algebra__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__normed__algebra = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__normed__algebra__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__normed__div__algebra = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__normed__field = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__normed__vector = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_RealVector_Oreal__vector = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Ocomm__ring__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Ocomm__semiring__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Odivision__by__zero = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Odivision__ring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Odvd = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Ofield = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oidom = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Olordered__ring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Omult__mono = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Omult__mono1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Omult__zero = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Ono__zero__divisors = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oordered__field = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oordered__idom = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oordered__ring__strict = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oordered__semidom = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Opordered__cancel__semiring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Opordered__ring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Opordered__ring__abs = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Opordered__semiring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oring = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oring__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oring__1__no__zero__divisors = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Oring__no__zero__divisors = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Osemiring__1 = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Osgn__if = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_class_Ring__and__Field_Ozero__neq__one = % 42.00/21.28 (\<lambda>x. _)(i1 := False, i2 := False, i3 := True) % 42.00/21.28 bnd_t_a = i3 % 42.00/21.28 bnd_tc_RealDef_Oreal = i3 % 42.00/21.28 bnd_v_x = i1 % 42.00/21.28 % SZS output end FiniteModel % 42.00/21.28 Total time: 11.3 s %------------------------------------------------------------------------------