%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : LCL649+1.015 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % Computer : n007.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 : Mon Sep 7 11:25:26 AM UTC 2026 % Result : CounterSatisfiable 201.23s 203.57s % Output : Model 201.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL649+1.015 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.05 % Command : /export/starexec/sandbox2/solver/bin/do_cvc5 /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT % 0.11/0.37 % Computer : n007.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sat Sep 5 10:26:09 UTC 2026 % 0.11/0.37 % CPUTime : % 0.28/0.69 %----Disproving FOF, CNF % 201.23/203.57 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 201.23/203.57 --- Run --no-e-matching --full-saturate-quant at 12... % 201.23/203.57 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 201.23/203.57 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 201.23/203.57 --- Run --multi-trigger-when-single --full-saturate-quant at 12... % 201.23/203.57 --- Run --trigger-sel=max --full-saturate-quant at 12... % 201.23/203.57 --- Run --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant at 12... % 201.23/203.57 --- Run --multi-trigger-cache --full-saturate-quant at 12... % 201.23/203.57 --- Run --prenex-quant=none --full-saturate-quant at 12... % 201.23/203.57 --- Run --enum-inst-interleave --decision=internal --full-saturate-quant at 12... % 201.23/203.57 --- Run --relevant-triggers --full-saturate-quant at 12... % 201.23/203.57 --- Run --finite-model-find --e-matching --sort-inference --uf-ss-fair at 66... % 201.23/203.57 --- Run --pre-skolem-quant=on --full-saturate-quant at 12... % 201.23/203.57 --- Run --macros-quant --macros-quant-mode=all --full-saturate-quant at 12... % 201.23/203.57 --- Run --mbqi --mbqi-enum --mbqi-enum-choice-grammar --mbqi-enum-global-syms-grammar --no-cegqi --no-sygus-inst at 36... % 201.23/203.57 % SZS status CounterSatisfiable % 201.23/203.57 % SZS output start Model % 201.23/203.57 ( % 201.23/203.57 ; cardinality of $$unsorted is 107 % 201.23/203.57 ; rep: (as @$$unsorted_0 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_1 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_2 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_3 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_4 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_5 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_6 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_7 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_8 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_9 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_10 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_11 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_12 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_13 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_14 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_15 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_16 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_17 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_18 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_19 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_20 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_21 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_22 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_23 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_24 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_25 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_26 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_27 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_28 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_29 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_30 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_31 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_32 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_33 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_34 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_35 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_36 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_37 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_38 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_39 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_40 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_41 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_42 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_43 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_44 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_45 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_46 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_47 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_48 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_49 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_50 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_51 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_52 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_53 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_54 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_55 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_56 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_57 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_58 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_59 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_60 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_61 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_62 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_63 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_64 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_65 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_66 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_67 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_68 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_69 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_70 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_71 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_72 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_73 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_74 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_75 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_76 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_77 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_78 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_79 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_80 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_81 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_82 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_83 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_84 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_85 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_86 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_87 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_88 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_89 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_90 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_91 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_92 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_93 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_94 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_95 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_96 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_97 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_98 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_99 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_100 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_101 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_102 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_103 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_104 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_105 $$unsorted) % 201.23/203.57 ; rep: (as @$$unsorted_106 $$unsorted) % 201.23/203.57 (define-fun tptp.r1 ((_arg_1 $$unsorted) (_arg_2 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1615 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1515 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1415 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1315 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1215 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1115 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1015 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p915 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p815 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p715 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p615 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p515 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p415 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p315 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p215 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p115 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1614 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1514 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1414 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1314 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1214 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1114 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1014 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p914 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p814 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p714 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p614 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p514 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p414 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p314 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p214 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p114 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1613 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1513 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1413 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1313 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1213 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1113 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1013 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p913 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p813 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p713 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p613 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p513 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p413 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p313 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p213 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p113 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1612 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1512 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1412 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1312 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1212 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1112 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1012 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p912 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p812 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p712 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p612 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p512 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p412 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p312 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p212 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p112 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1611 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1511 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1411 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1311 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1211 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1111 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p1011 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p911 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p811 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p711 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p611 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p511 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p411 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p311 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p211 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p111 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1610 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1510 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1410 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1310 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1210 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1110 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1010 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p910 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p810 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p710 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p610 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p510 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p410 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p310 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p210 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p110 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1609 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1509 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1409 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1309 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1209 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1109 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1009 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p909 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p809 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p709 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p609 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p509 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p409 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p309 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p209 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p109 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1608 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1508 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1408 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1308 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1208 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1108 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1008 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p908 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p808 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p708 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p608 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p508 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p408 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p308 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p208 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p108 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1607 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1507 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1407 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1307 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1207 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1107 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1007 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p907 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p807 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p707 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p607 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p507 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p407 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p307 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p207 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p107 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1606 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1506 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1406 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1306 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1206 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1106 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1006 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p906 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p806 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p706 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p606 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p506 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p406 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p306 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p206 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p106 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1605 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1505 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1405 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1305 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1205 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1105 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1005 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p905 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p805 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p705 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p605 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p505 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p405 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p305 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p205 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p105 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1604 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1504 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1404 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1304 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1204 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1104 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1004 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p904 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p804 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p704 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p604 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p504 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p404 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.57 (define-fun tptp.p304 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p204 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p104 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1603 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1503 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1403 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.57 (define-fun tptp.p1303 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1203 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1103 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1003 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p903 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p803 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p703 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p603 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p503 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p403 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p303 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.58 (define-fun tptp.p203 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p103 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1602 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1502 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1402 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1302 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1202 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1102 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1002 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p902 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p802 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p702 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p602 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p502 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p402 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p302 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p202 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.58 (define-fun tptp.p102 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1601 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1501 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1401 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1301 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1201 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1101 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p1001 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p901 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p801 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p701 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p601 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p501 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p401 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p301 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p201 ((_arg_1 $$unsorted)) Bool false) % 201.23/203.58 (define-fun tptp.p101 ((_arg_1 $$unsorted)) Bool true) % 201.23/203.58 ) % 201.23/203.58 % SZS output end Model % 201.23/203.58 % cvc5 exiting %------------------------------------------------------------------------------