%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : NLP121-1 : TPTP v6.4.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n022.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:28:08 EDT 2016 % Result : Timeout 300.13s % 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 : NLP121-1 : TPTP v6.4.0. Released v2.4.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.23 % Computer : n022.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 : Tue Apr 5 12:59:54 CDT 2016 % 0.03/0.23 % CPUTime : % 6.30/5.83 > val it = (): unit % 6.50/6.06 Trying to find a model that refutes: True % 7.50/7.01 Unfolded term: [| !!U V W X Y. % 7.50/7.01 ((((((((((((((((~ bnd_city U V | ~ bnd_chevy U V) | ~ bnd_white U V) | % 7.50/7.01 ~ bnd_dirty U V) | % 7.50/7.01 ~ bnd_old U V) | % 7.50/7.01 ~ bnd_agent U W V) | % 7.50/7.01 ~ bnd_in U W V) | % 7.50/7.01 ~ bnd_placename U X) | % 7.50/7.01 ~ bnd_hollywood_placename U X) | % 7.50/7.01 ~ bnd_of U X V) | % 7.50/7.01 ~ bnd_event U W) | % 7.50/7.01 ~ bnd_present U W) | % 7.50/7.01 ~ bnd_barrel U W) | % 7.50/7.01 ~ bnd_down U W Y) | % 7.50/7.01 ~ bnd_lonely U Y) | % 7.50/7.01 ~ bnd_street U Y) | % 7.50/7.01 ~ bnd_actual_world U) | % 7.50/7.01 ~ bnd_ssSkC0; % 7.50/7.01 !!U V W X Y. % 7.50/7.01 ((((((((((((((((~ bnd_city U V | ~ bnd_street U V) | % 7.50/7.01 ~ bnd_lonely U V) | % 7.50/7.01 ~ bnd_down U W V) | % 7.50/7.01 ~ bnd_in U W V) | % 7.50/7.01 ~ bnd_placename U X) | % 7.50/7.01 ~ bnd_hollywood_placename U X) | % 7.50/7.01 ~ bnd_of U X V) | % 7.50/7.01 ~ bnd_event U W) | % 7.50/7.01 ~ bnd_present U W) | % 7.50/7.01 ~ bnd_barrel U W) | % 7.50/7.01 ~ bnd_agent U W Y) | % 7.50/7.01 ~ bnd_old U Y) | % 7.50/7.01 ~ bnd_dirty U Y) | % 7.50/7.01 ~ bnd_white U Y) | % 7.50/7.01 ~ bnd_chevy U Y) | % 7.50/7.01 ~ bnd_actual_world U) | % 7.50/7.01 bnd_ssSkC0; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_agent bnd_skc10 bnd_skc11 bnd_skc12; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_of bnd_skc10 bnd_skc14 bnd_skc13; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_in bnd_skc10 bnd_skc11 bnd_skc13; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_down bnd_skc10 bnd_skc11 bnd_skc13; % 7.50/7.01 bnd_ssSkC0 | bnd_down bnd_skc15 bnd_skc16 bnd_skc17; % 7.50/7.01 bnd_ssSkC0 | bnd_of bnd_skc15 bnd_skc19 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_in bnd_skc15 bnd_skc16 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_agent bnd_skc15 bnd_skc16 bnd_skc18; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_chevy bnd_skc10 bnd_skc12; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_white bnd_skc10 bnd_skc12; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_dirty bnd_skc10 bnd_skc12; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_old bnd_skc10 bnd_skc12; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_barrel bnd_skc10 bnd_skc11; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_present bnd_skc10 bnd_skc11; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_event bnd_skc10 bnd_skc11; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_hollywood_placename bnd_skc10 bnd_skc14; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_placename bnd_skc10 bnd_skc14; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_lonely bnd_skc10 bnd_skc13; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_street bnd_skc10 bnd_skc13; % 7.50/7.01 ~ bnd_ssSkC0 | bnd_city bnd_skc10 bnd_skc13; % 7.50/7.01 bnd_ssSkC0 | bnd_street bnd_skc15 bnd_skc17; % 7.50/7.01 bnd_ssSkC0 | bnd_lonely bnd_skc15 bnd_skc17; % 7.50/7.01 bnd_ssSkC0 | bnd_barrel bnd_skc15 bnd_skc16; % 7.50/7.01 bnd_ssSkC0 | bnd_present bnd_skc15 bnd_skc16; % 7.50/7.01 bnd_ssSkC0 | bnd_event bnd_skc15 bnd_skc16; % 7.50/7.01 bnd_ssSkC0 | bnd_hollywood_placename bnd_skc15 bnd_skc19; % 7.50/7.01 bnd_ssSkC0 | bnd_placename bnd_skc15 bnd_skc19; % 7.50/7.01 bnd_ssSkC0 | bnd_old bnd_skc15 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_dirty bnd_skc15 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_white bnd_skc15 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_chevy bnd_skc15 bnd_skc18; % 7.50/7.01 bnd_ssSkC0 | bnd_city bnd_skc15 bnd_skc18; bnd_actual_world bnd_skc10; % 7.50/7.01 bnd_actual_world bnd_skc15 |] % 7.50/7.01 ==> True % 7.50/7.01 Adding axioms... % 7.50/7.02 Typedef.type_definition_def % 10.31/9.91 ...done. % 10.41/9.91 Ground types: ?'b, TPTP_Interpret.ind % 10.41/9.91 Translating term (sizes: 1, 1) ... % 13.20/12.77 Invoking SAT solver... % 13.20/12.77 No model exists. % 13.20/12.77 Translating term (sizes: 2, 1) ... % 16.71/16.25 Invoking SAT solver... % 16.71/16.25 No model exists. % 16.71/16.25 Translating term (sizes: 1, 2) ... % 47.68/47.14 Invoking SAT solver... % 47.68/47.14 No model exists. % 47.68/47.14 Translating term (sizes: 3, 1) ... % 53.59/53.02 Invoking SAT solver... % 53.59/53.02 No model exists. % 53.59/53.02 Translating term (sizes: 2, 2) ... % 92.14/91.48 Invoking SAT solver... % 92.14/91.48 No model exists. % 92.14/91.48 Translating term (sizes: 1, 3) ... %------------------------------------------------------------------------------