%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SYN903-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 02:05:56 PM UTC 2026
% Result : Satisfiable 13.01s 2.59s
% Output : Saturation 13.01s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u459,negated_conjecture,
~ ssSkC10 ).
cnf(u464,negated_conjecture,
ssSkP370(skc21) ).
cnf(u468,negated_conjecture,
( ssSkP292(X0)
| ~ ssSkP301(X0) ) ).
cnf(u472,negated_conjecture,
( ssPv23(X0)
| ~ ssSkP301(X0) ) ).
cnf(u476,negated_conjecture,
( ssSkP294(X0)
| ~ ssSkP302(X0) ) ).
cnf(u480,negated_conjecture,
( ssPv13(X0)
| ~ ssSkP302(X0) ) ).
cnf(u484,negated_conjecture,
( ssSkP295(X0)
| ~ ssSkP303(X0) ) ).
cnf(u488,negated_conjecture,
( ssPv22(X0)
| ~ ssSkP303(X0) ) ).
cnf(u492,negated_conjecture,
( ssSkP298(X0)
| ~ ssSkP305(X0) ) ).
cnf(u496,negated_conjecture,
( ssPv21(X0)
| ~ ssSkP305(X0) ) ).
cnf(u500,negated_conjecture,
( ssSkP300(X0)
| ~ ssSkP306(X0) ) ).
cnf(u504,negated_conjecture,
( ssPv7(X0)
| ~ ssSkP306(X0) ) ).
cnf(u508,negated_conjecture,
( ssSkP293(X0)
| ~ ssSkP307(X0) ) ).
cnf(u512,negated_conjecture,
( ssPv16(X0)
| ~ ssSkP307(X0) ) ).
cnf(u516,negated_conjecture,
( ssSkP299(X0)
| ~ ssSkP308(X0) ) ).
cnf(u520,negated_conjecture,
( ssPv5(X0)
| ~ ssSkP308(X0) ) ).
cnf(u524,negated_conjecture,
( ssSkP297(X0)
| ~ ssSkP309(X0) ) ).
cnf(u528,negated_conjecture,
( ssPv15(X0)
| ~ ssSkP309(X0) ) ).
cnf(u532,negated_conjecture,
( ssSkP296(X0)
| ~ ssSkP310(X0) ) ).
cnf(u536,negated_conjecture,
( ssPv6(X0)
| ~ ssSkP310(X0) ) ).
cnf(u540,negated_conjecture,
( ssSkP280(X0)
| ~ ssSkP311(X0) ) ).
cnf(u544,negated_conjecture,
( ssSkP304(X0)
| ~ ssSkP311(X0) ) ).
cnf(u548,negated_conjecture,
( ssSkP321(X0)
| ~ ssSkP322(X0) ) ).
cnf(u552,negated_conjecture,
( ssSkP320(X0)
| ~ ssSkP324(X0) ) ).
cnf(u556,negated_conjecture,
( ssSkP323(X0)
| ~ ssSkP324(X0) ) ).
cnf(u560,negated_conjecture,
( ssSkP319(X0)
| ~ ssSkP326(X0) ) ).
cnf(u564,negated_conjecture,
( ssSkP325(X0)
| ~ ssSkP326(X0) ) ).
cnf(u568,negated_conjecture,
( ssSkP318(X0)
| ~ ssSkP328(X0) ) ).
cnf(u572,negated_conjecture,
( ssSkP327(X0)
| ~ ssSkP328(X0) ) ).
cnf(u576,negated_conjecture,
( ssSkP329(X0)
| ~ ssSkP330(X0) ) ).
cnf(u580,negated_conjecture,
( ssSkP331(X0)
| ~ ssSkP332(X0) ) ).
cnf(u584,negated_conjecture,
( ssSkP333(X0)
| ~ ssSkP334(X0) ) ).
cnf(u588,negated_conjecture,
( ssSkP335(X0)
| ~ ssSkP336(X0) ) ).
cnf(u592,negated_conjecture,
( ssSkP337(X0)
| ~ ssSkP338(X0) ) ).
cnf(u596,negated_conjecture,
( ssSkP317(X0)
| ~ ssSkP340(X0) ) ).
cnf(u600,negated_conjecture,
( ssSkP339(X0)
| ~ ssSkP340(X0) ) ).
cnf(u604,negated_conjecture,
( ssSkP341(X0)
| ~ ssSkP342(X0) ) ).
cnf(u608,negated_conjecture,
( ssSkP316(X0)
| ~ ssSkP344(X0) ) ).
cnf(u612,negated_conjecture,
( ssSkP343(X0)
| ~ ssSkP344(X0) ) ).
cnf(u616,negated_conjecture,
( ssSkP315(X0)
| ~ ssSkP346(X0) ) ).
cnf(u620,negated_conjecture,
( ssSkP345(X0)
| ~ ssSkP346(X0) ) ).
cnf(u624,negated_conjecture,
( ssSkP347(X0)
| ~ ssSkP348(X0) ) ).
cnf(u628,negated_conjecture,
( ssSkP349(X0)
| ~ ssSkP350(X0) ) ).
cnf(u632,negated_conjecture,
( ssSkP351(X0)
| ~ ssSkP352(X0) ) ).
cnf(u636,negated_conjecture,
( ssSkP353(X0)
| ~ ssSkP354(X0) ) ).
cnf(u640,negated_conjecture,
( ssSkP314(X0)
| ~ ssSkP356(X0) ) ).
cnf(u644,negated_conjecture,
( ssSkP355(X0)
| ~ ssSkP356(X0) ) ).
cnf(u648,negated_conjecture,
( ssSkP313(X0)
| ~ ssSkP358(X0) ) ).
cnf(u652,negated_conjecture,
( ssSkP357(X0)
| ~ ssSkP358(X0) ) ).
cnf(u656,negated_conjecture,
( ssSkP312(X0)
| ~ ssSkP360(X0) ) ).
cnf(u660,negated_conjecture,
( ssSkP359(X0)
| ~ ssSkP360(X0) ) ).
cnf(u664,negated_conjecture,
( ssSkP361(X0)
| ~ ssSkP362(X0) ) ).
cnf(u668,negated_conjecture,
( ssSkP363(X0)
| ~ ssSkP364(X0) ) ).
cnf(u672,negated_conjecture,
( ssSkP365(X0)
| ~ ssSkP366(X0) ) ).
cnf(u676,negated_conjecture,
( ssSkP367(X0)
| ~ ssSkP368(X0) ) ).
cnf(u680,negated_conjecture,
( ssSkP369(X0)
| ~ ssSkP370(X0) ) ).
cnf(u684,negated_conjecture,
( ssSkP282(skf54(X0))
| ~ ssSkP292(X0) ) ).
cnf(u688,negated_conjecture,
( ssSkP287(skf55(X0))
| ~ ssSkP293(X0) ) ).
cnf(u692,negated_conjecture,
( ssSkP283(skf56(X0))
| ~ ssSkP294(X0) ) ).
cnf(u696,negated_conjecture,
( ssSkP286(skf57(X0))
| ~ ssSkP295(X0) ) ).
cnf(u700,negated_conjecture,
( ssSkP289(skf58(X0))
| ~ ssSkP296(X0) ) ).
cnf(u704,negated_conjecture,
( ssSkP284(skf59(X0))
| ~ ssSkP297(X0) ) ).
cnf(u708,negated_conjecture,
( ssSkP290(skf60(X0))
| ~ ssSkP298(X0) ) ).
cnf(u712,negated_conjecture,
( ssSkP288(skf61(X0))
| ~ ssSkP299(X0) ) ).
cnf(u716,negated_conjecture,
( ssSkP285(skf62(X0))
| ~ ssSkP300(X0) ) ).
cnf(u720,negated_conjecture,
( ssSkP301(skf63(X0))
| ~ ssSkP312(X0) ) ).
cnf(u724,negated_conjecture,
( ssSkP303(skf64(X0))
| ~ ssSkP313(X0) ) ).
cnf(u728,negated_conjecture,
( ssSkP305(skf65(X0))
| ~ ssSkP314(X0) ) ).
cnf(u732,negated_conjecture,
( ssSkP307(skf66(X0))
| ~ ssSkP315(X0) ) ).
cnf(u736,negated_conjecture,
( ssSkP309(skf67(X0))
| ~ ssSkP316(X0) ) ).
cnf(u740,negated_conjecture,
( ssSkP302(skf68(X0))
| ~ ssSkP317(X0) ) ).
cnf(u744,negated_conjecture,
( ssSkP306(skf69(X0))
| ~ ssSkP318(X0) ) ).
cnf(u748,negated_conjecture,
( ssSkP310(skf70(X0))
| ~ ssSkP319(X0) ) ).
cnf(u752,negated_conjecture,
( ssSkP308(skf71(X0))
| ~ ssSkP320(X0) ) ).
cnf(u756,negated_conjecture,
( ~ ssPv23(skf45(X0))
| ~ ssSkP282(X0) ) ).
cnf(u760,negated_conjecture,
( ~ ssPv13(skf46(X0))
| ~ ssSkP283(X0) ) ).
cnf(u764,negated_conjecture,
( ~ ssPv15(skf47(X0))
| ~ ssSkP284(X0) ) ).
cnf(u768,negated_conjecture,
( ~ ssPv7(skf48(X0))
| ~ ssSkP285(X0) ) ).
cnf(u772,negated_conjecture,
( ~ ssPv22(skf49(X0))
| ~ ssSkP286(X0) ) ).
cnf(u776,negated_conjecture,
( ~ ssPv16(skf50(X0))
| ~ ssSkP287(X0) ) ).
cnf(u780,negated_conjecture,
( ~ ssPv5(skf51(X0))
| ~ ssSkP288(X0) ) ).
cnf(u784,negated_conjecture,
( ~ ssPv6(skf52(X0))
| ~ ssSkP289(X0) ) ).
cnf(u788,negated_conjecture,
( ~ ssPv21(skf53(X0))
| ~ ssSkP290(X0) ) ).
cnf(u801,negated_conjecture,
( ssRr(X0,skf44(X0))
| ~ ssSkP280(X0) ) ).
cnf(u805,negated_conjecture,
( ~ ssSkP301(skf45(X0))
| ~ ssSkP282(X0) ) ).
cnf(u809,negated_conjecture,
( ~ ssSkP302(skf46(X0))
| ~ ssSkP283(X0) ) ).
cnf(u813,negated_conjecture,
( ~ ssSkP309(skf47(X0))
| ~ ssSkP284(X0) ) ).
cnf(u817,negated_conjecture,
( ~ ssSkP306(skf48(X0))
| ~ ssSkP285(X0) ) ).
cnf(u821,negated_conjecture,
( ~ ssSkP303(skf49(X0))
| ~ ssSkP286(X0) ) ).
cnf(u825,negated_conjecture,
( ~ ssSkP307(skf50(X0))
| ~ ssSkP287(X0) ) ).
cnf(u829,negated_conjecture,
( ~ ssSkP308(skf51(X0))
| ~ ssSkP288(X0) ) ).
cnf(u833,negated_conjecture,
( ~ ssSkP310(skf52(X0))
| ~ ssSkP289(X0) ) ).
cnf(u837,negated_conjecture,
( ~ ssSkP305(skf53(X0))
| ~ ssSkP290(X0) ) ).
cnf(u841,negated_conjecture,
( ssRr(X0,skf45(X0))
| ~ ssSkP282(X0) ) ).
cnf(u845,negated_conjecture,
( ssRr(X0,skf46(X0))
| ~ ssSkP283(X0) ) ).
cnf(u849,negated_conjecture,
( ssRr(X0,skf47(X0))
| ~ ssSkP284(X0) ) ).
cnf(u853,negated_conjecture,
( ssRr(X0,skf48(X0))
| ~ ssSkP285(X0) ) ).
cnf(u857,negated_conjecture,
( ssRr(X0,skf49(X0))
| ~ ssSkP286(X0) ) ).
cnf(u861,negated_conjecture,
( ssRr(X0,skf50(X0))
| ~ ssSkP287(X0) ) ).
cnf(u865,negated_conjecture,
( ssRr(X0,skf51(X0))
| ~ ssSkP288(X0) ) ).
cnf(u869,negated_conjecture,
( ssRr(X0,skf52(X0))
| ~ ssSkP289(X0) ) ).
cnf(u873,negated_conjecture,
( ssRr(X0,skf53(X0))
| ~ ssSkP290(X0) ) ).
cnf(u877,negated_conjecture,
( ssRr(skf54(X0),X0)
| ~ ssSkP292(X0) ) ).
cnf(u881,negated_conjecture,
( ssRr(skf55(X0),X0)
| ~ ssSkP293(X0) ) ).
cnf(u885,negated_conjecture,
( ssRr(skf56(X0),X0)
| ~ ssSkP294(X0) ) ).
cnf(u889,negated_conjecture,
( ssRr(skf57(X0),X0)
| ~ ssSkP295(X0) ) ).
cnf(u893,negated_conjecture,
( ssRr(skf58(X0),X0)
| ~ ssSkP296(X0) ) ).
cnf(u897,negated_conjecture,
( ssRr(skf59(X0),X0)
| ~ ssSkP297(X0) ) ).
cnf(u901,negated_conjecture,
( ssRr(skf60(X0),X0)
| ~ ssSkP298(X0) ) ).
cnf(u905,negated_conjecture,
( ssRr(skf61(X0),X0)
| ~ ssSkP299(X0) ) ).
cnf(u909,negated_conjecture,
( ssRr(skf62(X0),X0)
| ~ ssSkP300(X0) ) ).
cnf(u913,negated_conjecture,
( ssRr(X0,skf63(X0))
| ~ ssSkP312(X0) ) ).
cnf(u917,negated_conjecture,
( ssRr(X0,skf64(X0))
| ~ ssSkP313(X0) ) ).
cnf(u921,negated_conjecture,
( ssRr(X0,skf65(X0))
| ~ ssSkP314(X0) ) ).
cnf(u925,negated_conjecture,
( ssRr(X0,skf66(X0))
| ~ ssSkP315(X0) ) ).
cnf(u929,negated_conjecture,
( ssRr(X0,skf67(X0))
| ~ ssSkP316(X0) ) ).
cnf(u933,negated_conjecture,
( ssRr(X0,skf68(X0))
| ~ ssSkP317(X0) ) ).
cnf(u937,negated_conjecture,
( ssRr(X0,skf69(X0))
| ~ ssSkP318(X0) ) ).
cnf(u941,negated_conjecture,
( ssRr(X0,skf70(X0))
| ~ ssSkP319(X0) ) ).
cnf(u945,negated_conjecture,
( ssRr(X0,skf71(X0))
| ~ ssSkP320(X0) ) ).
cnf(u949,negated_conjecture,
( ssRr(X0,skf72(X0))
| ~ ssSkP322(X0) ) ).
cnf(u953,negated_conjecture,
( ssRr(X0,skf73(X0))
| ~ ssSkP330(X0) ) ).
cnf(u957,negated_conjecture,
( ssRr(X0,skf74(X0))
| ~ ssSkP332(X0) ) ).
cnf(u961,negated_conjecture,
( ssRr(X0,skf75(X0))
| ~ ssSkP334(X0) ) ).
cnf(u965,negated_conjecture,
( ssRr(X0,skf76(X0))
| ~ ssSkP336(X0) ) ).
cnf(u969,negated_conjecture,
( ssRr(X0,skf77(X0))
| ~ ssSkP338(X0) ) ).
cnf(u973,negated_conjecture,
( ssRr(X0,skf78(X0))
| ~ ssSkP342(X0) ) ).
cnf(u977,negated_conjecture,
( ssRr(X0,skf79(X0))
| ~ ssSkP348(X0) ) ).
cnf(u981,negated_conjecture,
( ssRr(X0,skf80(X0))
| ~ ssSkP350(X0) ) ).
cnf(u985,negated_conjecture,
( ssRr(X0,skf81(X0))
| ~ ssSkP352(X0) ) ).
cnf(u989,negated_conjecture,
( ssRr(X0,skf82(X0))
| ~ ssSkP354(X0) ) ).
cnf(u993,negated_conjecture,
( ssRr(X0,skf83(X0))
| ~ ssSkP362(X0) ) ).
cnf(u997,negated_conjecture,
( ssRr(X0,skf84(X0))
| ~ ssSkP364(X0) ) ).
cnf(u1001,negated_conjecture,
( ssRr(X0,skf85(X0))
| ~ ssSkP366(X0) ) ).
cnf(u1005,negated_conjecture,
( ssRr(X0,skf86(X0))
| ~ ssSkP368(X0) ) ).
cnf(u1009,negated_conjecture,
( ssRr(X0,skf87(X0))
| ~ ssSkP370(X0) ) ).
cnf(u1013,negated_conjecture,
( ssSkP368(X0)
| ~ ssSkP369(X1)
| ~ ssSkP291(X0,X1) ) ).
cnf(u1017,negated_conjecture,
( ssSkP366(X0)
| ~ ssSkP367(X1)
| ~ ssSkP291(X0,X1) ) ).
cnf(u1021,negated_conjecture,
( ssSkP291(X2,X0)
| ~ ssSkP281(X2,X1)
| ~ ssRr(X0,X1) ) ).
cnf(u1025,negated_conjecture,
( ssSkP281(X2,X1)
| ~ ssRr(X0,X2)
| ~ ssRr(X0,X1) ) ).
cnf(u1029,negated_conjecture,
( ssSkP364(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP365(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1033,negated_conjecture,
( ssSkP362(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP363(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1037,negated_conjecture,
( ssSkP360(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP361(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1041,negated_conjecture,
( ssSkP358(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP359(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1045,negated_conjecture,
( ssSkP356(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP357(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1049,negated_conjecture,
( ssSkP354(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP355(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1053,negated_conjecture,
( ssSkP352(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP353(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1057,negated_conjecture,
( ssSkP350(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP351(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1061,negated_conjecture,
( ssSkP348(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP349(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1065,negated_conjecture,
( ssSkP346(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP347(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1069,negated_conjecture,
( ssSkP344(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP345(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1073,negated_conjecture,
( ssSkP342(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP343(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1077,negated_conjecture,
( ssSkP340(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP341(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1081,negated_conjecture,
( ssSkP338(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP339(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1085,negated_conjecture,
( ssSkP336(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP337(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1089,negated_conjecture,
( ssSkP334(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP335(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1093,negated_conjecture,
( ssSkP332(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP333(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1097,negated_conjecture,
( ssSkP330(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP331(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1101,negated_conjecture,
( ssSkP328(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP329(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1105,negated_conjecture,
( ssSkP326(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP327(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1109,negated_conjecture,
( ssSkP324(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP325(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1113,negated_conjecture,
( ssSkP322(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP323(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1117,negated_conjecture,
( ssSkP311(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP321(X3)
| ~ ssRr(X0,X1) ) ).
cnf(u1121,negated_conjecture,
( ssSkP280(X2)
| ~ ssRr(X0,X2)
| ~ ssRr(X3,X1)
| ~ ssSkP304(X3)
| ~ ssRr(X0,X1) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN903-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 17:14:02 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.21/2.23 % (2785040)Input is clausal, will run a generic CNF schedule.
% 11.21/2.23 % (2785049)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2465777881:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.21/2.23 % (2785049)Instruction limit reached!
% 11.21/2.23 % (2785049)------------------------------
% 11.21/2.23 % (2785049)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.23 % (2785049)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.23 % (2785049)CaDiCaL version: 2.1.3
% 11.21/2.23 % (2785049)Termination reason: Instruction limit
% 11.21/2.23 % (2785049)Termination phase: Saturation
% 11.21/2.23 % (2785049)Time elapsed: 0.030 s
% 11.21/2.23 % (2785049)Peak memory usage: 89 MB
% 11.21/2.23 % (2785049)Instructions burned: 115 (million)
% 11.21/2.23 % (2785046)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=680187607:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.21/2.23 % (2785047)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=240470990:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.21/2.23 % (2785048)lrs+10_1_sil=8000:sp=occurrence:random_seed=4196346687:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.21/2.23 % (2785045)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1609668020:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.21/2.23 % (2785051)dis-21_1_sil=8000:lcm=predicate:random_seed=3831547785:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 11.21/2.23 % (2785050)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2452956101:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.21/2.23 % (2785050)Refutation not found, incomplete strategy
% 11.21/2.23 % (2785050)------------------------------
% 11.21/2.23 % (2785050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.23 % (2785050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.23 % (2785050)CaDiCaL version: 2.1.3
% 11.21/2.23 % (2785050)Termination reason: Refutation not found, incomplete strategy
% 11.21/2.23 % (2785050)Time elapsed: 0.006 s
% 11.21/2.23 % (2785050)Peak memory usage: 88 MB
% 11.21/2.23 % (2785050)Instructions burned: 10 (million)
% 11.21/2.23 % (2785051)Instruction limit reached!
% 11.21/2.23 % (2785051)------------------------------
% 11.21/2.23 % (2785051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.23 % (2785051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.23 % (2785051)CaDiCaL version: 2.1.3
% 11.21/2.23 % (2785051)Termination reason: Instruction limit
% 11.21/2.23 % (2785051)Termination phase: Saturation
% 11.21/2.23 % (2785051)Time elapsed: 0.042 s
% 11.21/2.23 % (2785051)Peak memory usage: 88 MB
% 11.21/2.23 % (2785051)Instructions burned: 120 (million)
% 11.21/2.23 % (2785048)Instruction limit reached!
% 11.21/2.23 % (2785048)------------------------------
% 11.21/2.23 % (2785048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.23 % (2785048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.23 % (2785048)CaDiCaL version: 2.1.3
% 11.21/2.23 % (2785048)Termination reason: Instruction limit
% 11.21/2.23 % (2785048)Termination phase: Saturation
% 11.21/2.23 % (2785048)Time elapsed: 0.052 s
% 11.21/2.23 % (2785048)Peak memory usage: 90 MB
% 11.21/2.23 % (2785048)Instructions burned: 109 (million)
% 11.21/2.23 % (2785053)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2054902797:i=143:sd=2:aac=none:ss=axioms:sgt=16_2998 on theBenchmark for (2998ds/143Mi)
% 11.21/2.23 % (2785053)Instruction limit reached!
% 11.21/2.23 % (2785053)------------------------------
% 11.21/2.23 % (2785053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.21/2.23 % (2785053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.21/2.23 % (2785053)CaDiCaL version: 2.1.3
% 11.21/2.23 % (2785053)Termination reason: Instruction limit
% 11.21/2.23 % (2785053)Termination phase: Saturation
% 11.21/2.23 % (2785053)Time elapsed: 0.039 s
% 11.21/2.23 % (2785053)Peak memory usage: 90 MB
% 11.21/2.23 % (2785053)Instructions burned: 146 (million)
% 11.21/2.23 % (2785060)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=765560578:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 13.01/2.58 % (2785061)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1990866256:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 13.01/2.58 % (2785063)lrs+10_64_to=lpo:sil=8000:random_seed=3744165311:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 13.01/2.58 % (2785050)------------------------------
% 13.01/2.58 % (2785050)------------------------------
% 13.01/2.58 % (2785063)Instruction limit reached!
% 13.01/2.58 % (2785063)------------------------------
% 13.01/2.58 % (2785063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.58 % (2785063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.58 % (2785063)CaDiCaL version: 2.1.3
% 13.01/2.58 % (2785063)Termination reason: Instruction limit
% 13.01/2.58 % (2785063)Termination phase: Saturation
% 13.01/2.58 % (2785063)Time elapsed: 0.039 s
% 13.01/2.58 % (2785063)Peak memory usage: 92 MB
% 13.01/2.59 % (2785063)Instructions burned: 126 (million)
% 13.01/2.59 % (2785060)Instruction limit reached!
% 13.01/2.59 % (2785060)------------------------------
% 13.01/2.59 % (2785060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785060)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785060)Termination reason: Instruction limit
% 13.01/2.59 % (2785060)Termination phase: Saturation
% 13.01/2.59 % (2785060)Time elapsed: 0.095 s
% 13.01/2.59 % (2785060)Peak memory usage: 89 MB
% 13.01/2.59 % (2785060)Instructions burned: 191 (million)
% 13.01/2.59 % (2785061)Instruction limit reached!
% 13.01/2.59 % (2785061)------------------------------
% 13.01/2.59 % (2785061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785061)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785061)Termination reason: Instruction limit
% 13.01/2.59 % (2785061)Termination phase: Saturation
% 13.01/2.59 % (2785061)Time elapsed: 0.099 s
% 13.01/2.59 % (2785061)Peak memory usage: 91 MB
% 13.01/2.59 % (2785061)Instructions burned: 220 (million)
% 13.01/2.59 % (2785068)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=1168830231:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 13.01/2.59 % (2785067)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1283839805:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 13.01/2.59 % (2785067)Refutation not found, incomplete strategy
% 13.01/2.59 % (2785067)------------------------------
% 13.01/2.59 % (2785067)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785067)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785067)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.59 % (2785067)Time elapsed: 0.004 s
% 13.01/2.59 % (2785067)Peak memory usage: 88 MB
% 13.01/2.59 % (2785067)Instructions burned: 6 (million)
% 13.01/2.59 % (2785068)Instruction limit reached!
% 13.01/2.59 % (2785068)------------------------------
% 13.01/2.59 % (2785068)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785068)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785068)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785068)Termination reason: Instruction limit
% 13.01/2.59 % (2785068)Termination phase: Saturation
% 13.01/2.59 % (2785068)Time elapsed: 0.041 s
% 13.01/2.59 % (2785068)Peak memory usage: 91 MB
% 13.01/2.59 % (2785068)Instructions burned: 159 (million)
% 13.01/2.59 % (2785069)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2376285959:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 13.01/2.59 % (2785070)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2829048969:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2995 on theBenchmark for (2995ds/106Mi)
% 13.01/2.59 % (2785070)Instruction limit reached!
% 13.01/2.59 % (2785070)------------------------------
% 13.01/2.59 % (2785070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785070)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785070)Termination reason: Instruction limit
% 13.01/2.59 % (2785070)Termination phase: Saturation
% 13.01/2.59 % (2785070)Time elapsed: 0.059 s
% 13.01/2.59 % (2785070)Peak memory usage: 90 MB
% 13.01/2.59 % (2785070)Instructions burned: 107 (million)
% 13.01/2.59 % (2785074)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4129677801:i=107_2993 on theBenchmark for (2993ds/107Mi)
% 13.01/2.59 % (2785074)Instruction limit reached!
% 13.01/2.59 % (2785074)------------------------------
% 13.01/2.59 % (2785074)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785074)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785074)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785074)Termination reason: Instruction limit
% 13.01/2.59 % (2785074)Termination phase: Saturation
% 13.01/2.59 % (2785074)Time elapsed: 0.033 s
% 13.01/2.59 % (2785074)Peak memory usage: 92 MB
% 13.01/2.59 % (2785074)Instructions burned: 107 (million)
% 13.01/2.59 % (2785067)------------------------------
% 13.01/2.59 % (2785067)------------------------------
% 13.01/2.59 % (2785076)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=892859295:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 13.01/2.59 % (2785076)Refutation not found, incomplete strategy
% 13.01/2.59 % (2785076)------------------------------
% 13.01/2.59 % (2785076)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785076)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785076)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785076)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.59 % (2785076)Time elapsed: 0.007 s
% 13.01/2.59 % (2785076)Peak memory usage: 88 MB
% 13.01/2.59 % (2785076)Instructions burned: 12 (million)
% 13.01/2.59 % (2785078)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2212516275:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 13.01/2.59 % (2785079)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1597299439:i=134:sd=2:doe=on:ss=axioms:sgt=14_2991 on theBenchmark for (2991ds/134Mi)
% 13.01/2.59 % (2785079)Refutation not found, incomplete strategy
% 13.01/2.59 % (2785079)------------------------------
% 13.01/2.59 % (2785079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785079)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785079)Termination reason: Refutation not found, incomplete strategy
% 13.01/2.59 % (2785079)Time elapsed: 0.007 s
% 13.01/2.59 % (2785079)Peak memory usage: 88 MB
% 13.01/2.59 % (2785079)Instructions burned: 11 (million)
% 13.01/2.59 % (2785076)------------------------------
% 13.01/2.59 % (2785076)------------------------------
% 13.01/2.59 % (2785079)------------------------------
% 13.01/2.59 % (2785079)------------------------------
% 13.01/2.59 % (2785083)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2573381947:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 13.01/2.59 % (2785084)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3054407167:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 13.01/2.59 % (2785084)Instruction limit reached!
% 13.01/2.59 % (2785084)------------------------------
% 13.01/2.59 % (2785084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785084)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785084)Termination reason: Instruction limit
% 13.01/2.59 % (2785084)Termination phase: Saturation
% 13.01/2.59 % (2785084)Time elapsed: 0.096 s
% 13.01/2.59 % (2785084)Peak memory usage: 92 MB
% 13.01/2.59 % (2785084)Instructions burned: 191 (million)
% 13.01/2.59 % (2785083)Instruction limit reached!
% 13.01/2.59 % (2785083)------------------------------
% 13.01/2.59 % (2785083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785083)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785083)Termination reason: Instruction limit
% 13.01/2.59 % (2785083)Termination phase: Saturation
% 13.01/2.59 % (2785083)Time elapsed: 0.257 s
% 13.01/2.59 % (2785083)Peak memory usage: 93 MB
% 13.01/2.59 % (2785083)Instructions burned: 500 (million)
% 13.01/2.59 % (2785087)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2621342835:i=264:kws=precedence:fsr=off_2984 on theBenchmark for (2984ds/264Mi)
% 13.01/2.59 % (2785087)First to succeed.
% 13.01/2.59 % (2785087)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2785040"
% 13.01/2.59 % (2785088)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=2616463001:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 13.01/2.59 % (2785088)Instruction limit reached!
% 13.01/2.59 % (2785088)------------------------------
% 13.01/2.59 % (2785088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.01/2.59 % (2785088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.01/2.59 % (2785088)CaDiCaL version: 2.1.3
% 13.01/2.59 % (2785088)Termination reason: Instruction limit
% 13.01/2.59 % (2785088)Termination phase: Saturation
% 13.01/2.59 % (2785088)Time elapsed: 0.067 s
% 13.01/2.59 % (2785088)Peak memory usage: 89 MB
% 13.01/2.59 % (2785088)Instructions burned: 158 (million)
% 13.01/2.59 % SZS status Satisfiable for theBenchmark
% 13.01/2.59 % SZS output start Saturation.
% See solution above
% 13.01/2.59 % SZS output start Definitions and Model Updates.
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv11(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP110(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP111(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC4 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP128(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP127(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP126(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP161(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP162(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC6 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP187(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP186(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP185(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP163(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP164(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP165(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP166(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP167(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP168(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP169(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP170(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP171(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP172(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP173(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP174(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP175(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP176(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP177(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP178(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP179(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP180(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP181(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP182(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP183(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP184(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv27(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP125(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP124(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP123(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP112(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP113(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP114(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP115(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP116(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP117(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP118(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP119(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP120(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP121(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP122(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv25(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP0(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP1(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC0 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP28(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP27(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP2(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP3(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP4(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP5(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP6(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP7(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP8(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP9(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP10(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP11(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP12(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP13(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP14(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP15(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP16(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP17(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP18(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP19(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP20(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP21(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP22(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP23(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP24(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP25(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP26(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv28(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP61(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP62(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC2 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP81(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP80(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP79(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP78(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP77(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP76(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP75(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP74(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP73(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP72(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP71(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP70(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP63(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP64(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP65(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP66(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP67(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP68(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP69(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv19(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP218(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP219(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC8 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP249(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP248(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP247(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP246(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP82(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP83(X0,X1) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkC3 := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP109(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP108(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP107(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP106(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP105(X0) := $true
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP84(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP85(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP86(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP87(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP88(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP89(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP90(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP91(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP92(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP93(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP94(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP95(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP96(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP97(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP98(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP99(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP100(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP101(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP102(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP103(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssSkP104(X0) := $false
% 13.01/2.59 for all inputs,
% 13.01/2.59 define ssPv26(X0) := $false
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP245(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP244(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP243(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP242(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP241(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP240(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP239(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP238(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP237(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP236(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP235(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP234(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP233(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP232(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP231(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP230(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP229(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP228(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP227(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP226(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP225(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP224(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP223(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP222(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP221(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP220(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP129(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP130(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkC5 := $false
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP160(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP159(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP158(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP157(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP156(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP155(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP154(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP153(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP152(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP151(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP150(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP149(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP148(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP147(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP146(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP145(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP144(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP143(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP142(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP141(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP140(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP139(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP138(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP137(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP136(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP135(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP134(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP133(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP132(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP131(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP29(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP30(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkC1 := $false
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP60(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP59(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP58(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP57(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP56(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP55(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP54(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP53(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP52(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP51(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP50(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP49(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP48(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP47(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP46(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP45(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP44(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP43(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP42(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP41(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP40(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP39(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP38(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP37(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP36(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP35(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP34(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP33(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP32(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP31(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssPv2(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP250(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP251(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkC9 := $false
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP279(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP278(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP277(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP276(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP275(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP274(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP273(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP272(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP271(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP270(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP269(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP268(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP267(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP266(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP265(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP264(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP263(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP262(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP261(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP260(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP259(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP258(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP257(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP256(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP255(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP254(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP253(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP252(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP188(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP189(X0,X1) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkC7 := $false
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP217(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP216(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP215(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP214(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP213(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP212(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP211(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP210(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP209(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP208(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP207(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP206(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP205(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP204(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP203(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP202(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP201(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP200(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP199(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP198(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP197(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP196(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP195(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP194(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP193(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP192(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP191(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssSkP190(X0) := $true
% 14.12/2.78 for all inputs,
% 14.12/2.78 define ssPv4(X0) := $false
% 14.12/2.78 % SZS output end Definitions and Model Updates.
% 14.12/2.78 % (2785087)------------------------------
% 14.12/2.78 % (2785087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.12/2.78 % (2785087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.12/2.78 % (2785087)CaDiCaL version: 2.1.3
% 14.12/2.78 % (2785087)Termination reason: Satisfiable
% 14.12/2.78 % (2785087)Time elapsed: 0.010 s
% 14.12/2.78 % (2785087)Peak memory usage: 89 MB
% 14.12/2.78 % (2785087)Instructions burned: 14 (million)
% 14.12/2.78 % (2785087)------------------------------
% 14.12/2.78 % (2785087)------------------------------
% 14.12/2.78 % (2785040)Success in time 1.92 s
% 14.12/2.78 % Vampire exiting
%------------------------------------------------------------------------------