%------------------------------------------------------------------------------ % File : Refute---2015 % Problem : SWC194-1 : TPTP v6.4.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : isabelle tptp_refute %d %s % Computer : n053.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.10.1.el7.x86_64 % CPULimit : 300s % DateTime : Thu Apr 14 04:51:27 EDT 2016 % Result : Timeout 300.32s % 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 : SWC194-1 : TPTP v6.4.0. Released v2.4.0. % 0.00/0.04 % Command : isabelle tptp_refute %d %s % 0.03/0.22 % Computer : n053.star.cs.uiowa.edu % 0.03/0.22 % Model : x86_64 x86_64 % 0.03/0.22 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % 0.03/0.22 % Memory : 32218.75MB % 0.03/0.22 % OS : Linux 3.10.0-327.10.1.el7.x86_64 % 0.03/0.22 % CPULimit : 300 % 0.03/0.22 % DateTime : Fri Apr 8 21:10:39 CDT 2016 % 0.03/0.23 % CPUTime : % 6.30/5.94 > val it = (): unit % 6.71/6.38 Trying to find a model that refutes: True % 10.91/10.59 Unfolded term: [| ~ bnd_sk5 = bnd_sk6; % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_app (bnd_app bnd_sk7 (bnd_cons bnd_sk5 bnd_nil)) bnd_sk9) % 10.91/10.59 (bnd_cons bnd_sk6 bnd_nil)) % 10.91/10.59 bnd_sk8 = % 10.91/10.59 bnd_sk1; % 10.91/10.59 bnd_ssList bnd_sk9; bnd_ssList bnd_sk8; bnd_ssList bnd_sk7; % 10.91/10.59 bnd_ssItem bnd_sk6; bnd_ssItem bnd_sk5; % 10.91/10.59 !!A B C D. % 10.91/10.59 ((((~ bnd_ssItem A | ~ bnd_ssItem B) | ~ bnd_ssList C) | % 10.91/10.59 ~ bnd_ssList D) | % 10.91/10.59 A = B) | % 10.91/10.59 ~ bnd_app % 10.91/10.59 (bnd_app (bnd_app C (bnd_cons A bnd_nil)) (bnd_cons B bnd_nil)) D = % 10.91/10.59 bnd_sk3; % 10.91/10.59 bnd_sk1 = bnd_sk3; bnd_sk2 = bnd_sk4; bnd_ssList bnd_sk4; % 10.91/10.59 bnd_ssList bnd_sk3; bnd_ssList bnd_sk2; bnd_ssList bnd_sk1; % 10.91/10.59 !!U V W X Y Z. % 10.91/10.59 ((((((((~ bnd_leq U V | ~ bnd_leq V U) | % 10.91/10.59 ~ bnd_app (bnd_app W (bnd_cons U X)) (bnd_cons V Y) = Z) | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_cyclefreeP Z) | % 10.91/10.59 ~ bnd_ssList Z; % 10.91/10.59 !!U V W X Y Z. % 10.91/10.59 ((((((((~ bnd_app (bnd_app U (bnd_cons V W)) (bnd_cons X Y) = Z | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem X) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_totalorderP Z) | % 10.91/10.59 ~ bnd_ssList Z) | % 10.91/10.59 bnd_leq V X) | % 10.91/10.59 bnd_leq X V; % 10.91/10.59 !!U V W X Y Z. % 10.91/10.59 ((((((((~ bnd_app (bnd_app U (bnd_cons V W)) (bnd_cons X Y) = Z | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem X) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_strictorderP Z) | % 10.91/10.59 ~ bnd_ssList Z) | % 10.91/10.59 bnd_lt V X) | % 10.91/10.59 bnd_lt X V; % 10.91/10.59 !!U V W X Y Z. % 10.91/10.59 (((((((~ bnd_app (bnd_app U (bnd_cons V W)) (bnd_cons X Y) = Z | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem X) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_totalorderedP Z) | % 10.91/10.59 ~ bnd_ssList Z) | % 10.91/10.59 bnd_leq V X; % 10.91/10.59 !!U V W X Y Z. % 10.91/10.59 (((((((~ bnd_app (bnd_app U (bnd_cons V W)) (bnd_cons X Y) = Z | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem X) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_strictorderedP Z) | % 10.91/10.59 ~ bnd_ssList Z) | % 10.91/10.59 bnd_lt V X; % 10.91/10.59 !!U V W X Y. % 10.91/10.59 ((((((~ bnd_app U (bnd_cons V (bnd_cons W X)) = Y | ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_equalelemsP Y) | % 10.91/10.59 ~ bnd_ssList Y) | % 10.91/10.59 V = W; % 10.91/10.59 !!U V W X Y. % 10.91/10.59 (((((~ bnd_app (bnd_app U (bnd_cons V W)) (bnd_cons V X) = Y | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_duplicatefreeP Y) | % 10.91/10.59 ~ bnd_ssList Y; % 10.91/10.59 !!U V W X. % 10.91/10.59 (((((~ bnd_frontsegP U V | ~ W = X) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem X) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 bnd_frontsegP (bnd_cons W U) (bnd_cons X V); % 10.91/10.59 !!U V. % 10.91/10.59 (((((~ bnd_tl U = bnd_tl V | ~ bnd_hd U = bnd_hd V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 bnd_nil = V) | % 10.91/10.59 U = V) | % 10.91/10.59 bnd_nil = U; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_frontsegP (bnd_cons U V) (bnd_cons W X) | ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 U = W; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_app U (bnd_cons V W) = X | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 bnd_memberP X V; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_frontsegP (bnd_cons U V) (bnd_cons W X) | ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_frontsegP V X; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_app (bnd_app U V) W = X | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 bnd_segmentP X V; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_segmentP U V | ~ bnd_ssList W) | ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_segmentP (bnd_app (bnd_app X U) W) V; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_cons U V = bnd_cons W X | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 X = V; % 10.91/10.59 !!U V W X. % 10.91/10.59 ((((~ bnd_cons U V = bnd_cons W X | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_ssList X) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 U = W; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_memberP U V | ~ bnd_ssItem V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_app (bnd_skaf42 U V) (bnd_cons V (bnd_skaf43 V U)) = U; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_segmentP U V | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_app (bnd_app (bnd_skaf47 U V) V) (bnd_skaf48 V U) = U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_cyclefreeP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf51 U) (bnd_cons (bnd_skaf49 U) (bnd_skaf52 U))) % 10.91/10.59 (bnd_cons (bnd_skaf50 U) (bnd_skaf53 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_totalorderP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf56 U) (bnd_cons (bnd_skaf54 U) (bnd_skaf57 U))) % 10.91/10.59 (bnd_cons (bnd_skaf55 U) (bnd_skaf58 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_strictorderP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf61 U) (bnd_cons (bnd_skaf59 U) (bnd_skaf62 U))) % 10.91/10.59 (bnd_cons (bnd_skaf60 U) (bnd_skaf63 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_totalorderedP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf66 U) (bnd_cons (bnd_skaf64 U) (bnd_skaf67 U))) % 10.91/10.59 (bnd_cons (bnd_skaf65 U) (bnd_skaf68 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_strictorderedP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf71 U) (bnd_cons (bnd_skaf69 U) (bnd_skaf72 U))) % 10.91/10.59 (bnd_cons (bnd_skaf70 U) (bnd_skaf73 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_duplicatefreeP U) | % 10.91/10.59 bnd_app % 10.91/10.59 (bnd_app (bnd_skaf75 U) (bnd_cons (bnd_skaf74 U) (bnd_skaf76 U))) % 10.91/10.59 (bnd_cons (bnd_skaf74 U) (bnd_skaf77 U)) = % 10.91/10.59 U; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_memberP (bnd_cons U V) W | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 bnd_memberP V W) | % 10.91/10.59 W = U; % 10.91/10.59 !!U V. % 10.91/10.59 ((((~ bnd_lt U (bnd_hd V) | ~ bnd_strictorderedP V) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_strictorderedP (bnd_cons U V)) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 ((((~ bnd_leq U (bnd_hd V) | ~ bnd_totalorderedP V) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_totalorderedP (bnd_cons U V)) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_memberP (bnd_app U V) W | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem W) | % 10.91/10.59 bnd_memberP V W) | % 10.91/10.59 bnd_memberP U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((~ bnd_ssItem U | ~ bnd_ssList V) | ~ bnd_ssList W) | % 10.91/10.59 bnd_cons U (bnd_app V W) = bnd_app (bnd_cons U V) W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_leq U V | ~ bnd_leq V W) | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_leq U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_lt U V | ~ bnd_lt V W) | ~ bnd_ssItem W) | ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_lt U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_frontsegP U V | ~ bnd_frontsegP V W) | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_frontsegP U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_rearsegP U V | ~ bnd_rearsegP V W) | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_rearsegP U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_segmentP U V | ~ bnd_segmentP V W) | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_segmentP U W; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_app U V = bnd_app W V | ~ bnd_ssList U) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 U = W; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_app U V = bnd_app U W | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 V = W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((~ bnd_ssList U | ~ bnd_ssList V) | ~ bnd_ssList W) | % 10.91/10.59 bnd_app (bnd_app W V) U = bnd_app W (bnd_app V U); % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_geq U V | ~ bnd_geq V W) | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_geq U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_leq U V | ~ bnd_lt V W) | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_lt U W; % 10.91/10.59 !!U V W. % 10.91/10.59 ((((~ bnd_gt U V | ~ bnd_gt V W) | ~ bnd_ssItem W) | ~ bnd_ssItem V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_gt U W; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_nil = U | ~ bnd_nil = V) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_app U V = bnd_nil; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_app U V = W | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 bnd_frontsegP W U; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_app U V = W | ~ bnd_ssList U) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList W) | % 10.91/10.59 bnd_rearsegP W V; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_equalelemsP U) | % 10.91/10.59 bnd_app (bnd_skaf80 U) % 10.91/10.59 (bnd_cons (bnd_skaf78 U) % 10.91/10.59 (bnd_cons (bnd_skaf79 U) (bnd_skaf81 U))) = % 10.91/10.59 U; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_memberP U V | ~ bnd_ssList U) | ~ bnd_ssList W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 bnd_memberP (bnd_app W U) V; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_memberP U V | ~ bnd_ssList W) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 bnd_memberP (bnd_app U W) V; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_memberP U V | ~ bnd_ssList U) | ~ bnd_ssItem W) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 bnd_memberP (bnd_cons W U) V; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ U = V | ~ bnd_ssList W) | ~ bnd_ssItem V) | ~ bnd_ssItem U) | % 10.91/10.59 bnd_memberP (bnd_cons V W) U; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_frontsegP U V | ~ bnd_ssList W) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_frontsegP (bnd_app U W) V; % 10.91/10.59 !!U V W. % 10.91/10.59 (((~ bnd_rearsegP U V | ~ bnd_ssList W) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssList U) | % 10.91/10.59 bnd_rearsegP (bnd_app W U) V; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_totalorderedP (bnd_cons U V) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_leq U (bnd_hd V)) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_strictorderedP (bnd_cons U V) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_lt U (bnd_hd V)) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_ssList U | ~ bnd_ssList V) | bnd_nil = V) | % 10.91/10.59 bnd_tl (bnd_app V U) = bnd_app (bnd_tl V) U; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_frontsegP U V | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_app V (bnd_skaf45 U V) = U; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_rearsegP U V | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_app (bnd_skaf46 U V) V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_leq U V | ~ bnd_leq V U) | ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_frontsegP U V | ~ bnd_frontsegP V U) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_rearsegP U V | ~ bnd_rearsegP V U) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_segmentP U V | ~ bnd_segmentP V U) | ~ bnd_ssList U) | % 10.91/10.59 ~ bnd_ssList V) | % 10.91/10.59 V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_geq U V | ~ bnd_geq V U) | ~ bnd_ssItem U) | % 10.91/10.59 ~ bnd_ssItem V) | % 10.91/10.59 V = U; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_totalorderedP (bnd_cons U V) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_totalorderedP V) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_strictorderedP (bnd_cons U V) | ~ bnd_ssList V) | % 10.91/10.59 ~ bnd_ssItem U) | % 10.91/10.59 bnd_strictorderedP V) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_ssList U | ~ bnd_ssList V) | bnd_nil = V) | % 10.91/10.59 bnd_hd (bnd_app V U) = bnd_hd V; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_leq U V | ~ bnd_ssItem V) | ~ bnd_ssItem U) | bnd_lt U V) | % 10.91/10.59 U = V; % 10.91/10.59 !!U V. % 10.91/10.59 (((~ bnd_leq U V | ~ bnd_ssItem V) | ~ bnd_ssItem U) | bnd_lt U V) | % 10.91/10.59 U = V; % 10.91/10.59 !!U V. % 10.91/10.59 (~ bnd_ssItem U | ~ bnd_ssList V) | % 10.91/10.59 bnd_app (bnd_cons U bnd_nil) V = bnd_cons U V; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_app U V = bnd_nil | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_nil = V; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_app U V = bnd_nil | ~ bnd_ssList V) | ~ bnd_ssList U) | % 10.91/10.59 bnd_nil = U; % 10.91/10.59 !!U V. ((~ U = V | ~ bnd_neq U V) | ~ bnd_ssItem V) | ~ bnd_ssItem U; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_cons U bnd_nil = V | ~ bnd_ssItem U) | ~ bnd_ssList V) | % 10.91/10.59 bnd_singletonP V; % 10.91/10.59 !!U V. ((~ U = V | ~ bnd_neq U V) | ~ bnd_ssList V) | ~ bnd_ssList U; % 10.91/10.59 !!U V. ((~ bnd_lt U V | ~ bnd_lt V U) | ~ bnd_ssItem U) | ~ bnd_ssItem V; % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_nil = U | ~ bnd_ssList U) | ~ bnd_ssItem V) | % 10.91/10.59 bnd_totalorderedP (bnd_cons V U); % 10.91/10.59 !!U V. % 10.91/10.59 ((~ bnd_nil = U | ~ bnd_ssList U) | ~ bnd_ssItem V) | % 10.91/10.59 bnd_strictorderedP (bnd_cons V U); % 10.91/10.59 !!U V. ((~ U = V | ~ bnd_lt U V) | ~ bnd_ssItem V) | ~ bnd_ssItem U; % 10.91/10.59 !!U V. ((~ bnd_gt U V | ~ bnd_gt V U) | ~ bnd_ssItem U) | ~ bnd_ssItem V; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_cons (bnd_skaf83 U) (bnd_skaf82 U) = U) | % 10.91/10.59 bnd_nil = U; % 10.91/10.59 !!U V. ((~ bnd_leq U V | ~ bnd_ssItem U) | ~ bnd_ssItem V) | bnd_geq V U; % 10.91/10.59 !!U V. ((~ bnd_geq U V | ~ bnd_ssItem V) | ~ bnd_ssItem U) | bnd_leq V U; % 10.91/10.59 !!U V. ((~ bnd_lt U V | ~ bnd_ssItem U) | ~ bnd_ssItem V) | bnd_gt V U; % 10.91/10.59 !!U V. ((~ bnd_gt U V | ~ bnd_ssItem V) | ~ bnd_ssItem U) | bnd_lt V U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_cons (bnd_hd U) (bnd_tl U) = U) | bnd_nil = U; % 10.91/10.59 !!U V. ((~ bnd_lt U V | ~ bnd_ssItem V) | ~ bnd_ssItem U) | bnd_leq U V; % 10.91/10.59 !!U V. ((~ bnd_ssItem U | ~ bnd_ssItem V) | bnd_neq V U) | V = U; % 10.91/10.59 !!U. (~ bnd_singletonP U | ~ bnd_ssList U) | % 10.91/10.59 bnd_cons (bnd_skaf44 U) bnd_nil = U; % 10.91/10.59 !!U V. ((~ bnd_ssList U | ~ bnd_ssList V) | bnd_neq V U) | V = U; % 10.91/10.59 !!U V. (~ bnd_cons U V = V | ~ bnd_ssItem U) | ~ bnd_ssList V; % 10.91/10.59 !!U V. (~ bnd_cons U V = bnd_nil | ~ bnd_ssItem U) | ~ bnd_ssList V; % 10.91/10.59 !!U V. (~ bnd_ssItem U | ~ bnd_ssList V) | bnd_hd (bnd_cons U V) = U; % 10.91/10.59 !!U V. (~ bnd_ssItem U | ~ bnd_ssList V) | bnd_tl (bnd_cons U V) = V; % 10.91/10.59 !!U. (~ bnd_leq (bnd_skaf54 U) (bnd_skaf55 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_totalorderP U; % 10.91/10.59 !!U. (~ bnd_leq (bnd_skaf55 U) (bnd_skaf54 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_totalorderP U; % 10.91/10.59 !!U. (~ bnd_lt (bnd_skaf59 U) (bnd_skaf60 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_strictorderP U; % 10.91/10.59 !!U. (~ bnd_lt (bnd_skaf60 U) (bnd_skaf59 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_strictorderP U; % 10.91/10.59 !!U. (~ bnd_leq (bnd_skaf64 U) (bnd_skaf65 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_totalorderedP U; % 10.91/10.59 !!U. (~ bnd_lt (bnd_skaf69 U) (bnd_skaf70 U) | ~ bnd_ssList U) | % 10.91/10.59 bnd_strictorderedP U; % 10.91/10.59 !!U. (~ bnd_skaf79 U = bnd_skaf78 U | ~ bnd_ssList U) | % 10.91/10.59 bnd_equalelemsP U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_cyclefreeP U) | % 10.91/10.59 bnd_leq (bnd_skaf49 U) (bnd_skaf50 U); % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_cyclefreeP U) | % 10.91/10.59 bnd_leq (bnd_skaf50 U) (bnd_skaf49 U); % 10.91/10.59 !!U V. (~ bnd_ssItem U | ~ bnd_ssList V) | bnd_ssList (bnd_cons U V); % 10.91/10.59 !!U V. (~ bnd_ssList U | ~ bnd_ssList V) | bnd_ssList (bnd_app V U); % 10.91/10.59 !!U. (~ bnd_frontsegP bnd_nil U | ~ bnd_ssList U) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_nil = U | ~ bnd_ssList U) | bnd_frontsegP bnd_nil U; % 10.91/10.59 !!U. (~ bnd_rearsegP bnd_nil U | ~ bnd_ssList U) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_nil = U | ~ bnd_ssList U) | bnd_rearsegP bnd_nil U; % 10.91/10.59 !!U. (~ bnd_segmentP bnd_nil U | ~ bnd_ssList U) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_nil = U | ~ bnd_ssList U) | bnd_segmentP bnd_nil U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_ssItem (bnd_hd U)) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_ssList (bnd_tl U)) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_ssItem (bnd_hd U)) | bnd_nil = U; % 10.91/10.59 !!U. (~ bnd_ssList U | bnd_ssList (bnd_tl U)) | bnd_nil = U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_app bnd_nil U = U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_app U bnd_nil = U; % 10.91/10.59 !!U V. (~ bnd_ssList U | bnd_duplicatefreeP U) | bnd_ssItem V; % 10.91/10.59 !!U. ~ bnd_memberP bnd_nil U | ~ bnd_ssItem U; % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_cyclefreeP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_totalorderP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_strictorderP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_totalorderedP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_strictorderedP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_duplicatefreeP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_equalelemsP (bnd_cons U bnd_nil); % 10.91/10.59 !!U. ~ bnd_lt U U | ~ bnd_ssItem U; !!U. ~ bnd_ssItem U | bnd_leq U U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_frontsegP U U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_frontsegP U bnd_nil; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_rearsegP U U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_rearsegP U bnd_nil; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_segmentP U U; % 10.91/10.59 !!U. ~ bnd_ssList U | bnd_segmentP U bnd_nil; % 10.91/10.59 !!U. ~ bnd_ssItem U | bnd_geq U U; ~ bnd_skac3 = bnd_skac2; % 10.91/10.59 !!U V. bnd_ssList (bnd_skaf42 U V); !!U V. bnd_ssList (bnd_skaf43 U V); % 10.91/10.59 !!U V. bnd_ssList (bnd_skaf45 U V); !!U V. bnd_ssList (bnd_skaf46 U V); % 10.91/10.59 !!U V. bnd_ssList (bnd_skaf47 U V); !!U V. bnd_ssList (bnd_skaf48 U V); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf44 U); !!U. bnd_ssItem (bnd_skaf49 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf50 U); !!U. bnd_ssList (bnd_skaf51 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf52 U); !!U. bnd_ssList (bnd_skaf53 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf54 U); !!U. bnd_ssItem (bnd_skaf55 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf56 U); !!U. bnd_ssList (bnd_skaf57 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf58 U); !!U. bnd_ssItem (bnd_skaf59 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf60 U); !!U. bnd_ssList (bnd_skaf61 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf62 U); !!U. bnd_ssList (bnd_skaf63 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf64 U); !!U. bnd_ssItem (bnd_skaf65 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf66 U); !!U. bnd_ssList (bnd_skaf67 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf68 U); !!U. bnd_ssItem (bnd_skaf69 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf70 U); !!U. bnd_ssList (bnd_skaf71 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf72 U); !!U. bnd_ssList (bnd_skaf73 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf74 U); !!U. bnd_ssList (bnd_skaf75 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf76 U); !!U. bnd_ssList (bnd_skaf77 U); % 10.91/10.59 !!U. bnd_ssItem (bnd_skaf78 U); !!U. bnd_ssItem (bnd_skaf79 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf80 U); !!U. bnd_ssList (bnd_skaf81 U); % 10.91/10.59 !!U. bnd_ssList (bnd_skaf82 U); !!U. bnd_ssItem (bnd_skaf83 U); % 10.91/10.59 ~ bnd_singletonP bnd_nil; bnd_ssItem bnd_skac2; bnd_ssItem bnd_skac3; % 10.91/10.59 bnd_ssList bnd_nil; bnd_cyclefreeP bnd_nil; bnd_totalorderP bnd_nil; % 10.91/10.59 bnd_strictorderP bnd_nil; bnd_totalorderedP bnd_nil; % 10.91/10.59 bnd_strictorderedP bnd_nil; bnd_duplicatefreeP bnd_nil; % 10.91/10.59 bnd_equalelemsP bnd_nil |] % 10.91/10.59 ==> True % 10.91/10.59 Adding axioms... % 10.91/10.60 Typedef.type_definition_def % 30.44/30.01 ...done. % 30.44/30.04 Ground types: ?'b, TPTP_Interpret.ind % 30.44/30.04 Translating term (sizes: 1, 1) ... % 47.97/47.59 Invoking SAT solver... % 47.97/47.59 No model exists. % 47.97/47.59 Translating term (sizes: 2, 1) ... % 66.32/65.82 Invoking SAT solver... % 66.32/65.82 No model exists. % 66.32/65.82 Translating term (sizes: 1, 2) ... % 232.42/231.08 Invoking SAT solver... % 232.42/231.08 No model exists. % 232.42/231.08 Translating term (sizes: 3, 1) ... % 253.29/251.70 Invoking SAT solver... % 253.29/251.70 No model exists. % 253.29/251.70 Translating term (sizes: 2, 2) ... %------------------------------------------------------------------------------