%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : NUM815^5 : TPTP v6.4.0. Bugfixed v5.2.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n018.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16091.75MB % OS : Linux 3.10.0-327.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Thu Apr 14 01:56:39 EDT 2016 % Result : GaveUp 38.51s % Output : None % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : NUM815^5 : TPTP v6.4.0. Bugfixed v5.2.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.23 % Computer : n018.star.cs.uiowa.edu % 0.03/0.23 % Model : x86_64 x86_64 % 0.03/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.23 % Memory : 16091.75MB % 0.03/0.23 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.23 % CPULimit : 300 % 0.03/0.23 % DateTime : Wed Apr 6 06:40:24 CDT 2016 % 0.03/0.23 % CPUTime : % 6.35/5.92 > val it = (): unit % 6.44/6.09 Trying to find a model that refutes: bnd_cIND & bnd_cPETER_INDEQS bnd_c0 bnd_cS bnd_cPSI --> % 6.44/6.09 (ALL Xm Xn. EX Xk. bnd_cPSI Xm Xn = bnd_cS Xk) % 6.55/6.16 Unfolded term: [| bnd_cPETER_INDEQS = % 6.55/6.16 (%X0 S PSI. % 6.55/6.16 ((ALL Xn. PSI X0 Xn = S Xn) & % 6.55/6.16 (ALL Xm. PSI (S Xm) X0 = PSI Xm (S X0))) & % 6.55/6.16 (ALL Xm Xn. PSI (S Xm) (S Xn) = PSI Xm (PSI (S Xm) Xn))); % 6.55/6.16 bnd_cIND = % 6.55/6.16 (ALL Xp. Xp bnd_c0 & (ALL Xx. Xp Xx --> Xp (bnd_cS Xx)) --> All Xp) |] % 6.55/6.16 ==> bnd_cIND & bnd_cPETER_INDEQS bnd_c0 bnd_cS bnd_cPSI --> % 6.55/6.16 (ALL Xm Xn. EX Xk. bnd_cPSI Xm Xn = bnd_cS Xk) % 6.55/6.16 Adding axioms... % 6.55/6.17 Typedef.type_definition_def % 7.35/6.98 ...done. % 7.35/6.98 Ground types: ?'b, TPTP_Interpret.ind % 7.35/6.98 Translating term (sizes: 1, 1) ... % 7.94/7.50 Invoking SAT solver... % 7.94/7.50 No model exists. % 7.94/7.50 Translating term (sizes: 2, 1) ... % 9.05/8.65 Invoking SAT solver... % 9.05/8.65 No model exists. % 9.05/8.65 Translating term (sizes: 1, 2) ... % 18.16/17.72 Invoking SAT solver... % 18.16/17.72 No model exists. % 18.16/17.72 Translating term (sizes: 3, 1) ... % 21.77/21.38 Invoking SAT solver... % 21.77/21.38 No model exists. % 21.77/21.38 Translating term (sizes: 2, 2) ... % 38.51/38.01 Invoking SAT solver... % 38.51/38.02 No model exists. % 38.51/38.02 Translating term (sizes: 1, 3) ... % 38.51/38.08 Search terminated, number of Boolean variables (100000 allowed) exceeded. % 38.51/38.08 % SZS status Unknown %------------------------------------------------------------------------------