%------------------------------------------------------------------------------ % File : cvc5-SAT---1.3.4 % Problem : SYN424-1 : TPTP v9.2.1. Released v2.1.0. % Transfm : none % Format : tptp:raw % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % Computer : n011.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Jun 3 09:10:52 AM UTC 2026 % Result : Satisfiable 37.75s 37.93s % Output : Model 37.75s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN424-1 : TPTP v9.2.1. Released v2.1.0. % 0.00/0.13 % Command : /export/starexec/sandbox/solver/bin/do_cvc5 /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT % 0.16/0.34 % Computer : n011.cluster.edu % 0.16/0.34 % Model : x86_64 x86_64 % 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.34 % Memory : 8042.1875MB % 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue Jun 2 23:28:20 EDT 2026 % 0.16/0.35 % CPUTime : % 0.48/0.63 %----Disproving FOF, CNF % 0.48/0.64 --- Run --decision=internal --simplification=none --no-inst-no-entail --no-cbqi --full-saturate-quant at 12... % 12.64/12.87 --- Run --no-e-matching --full-saturate-quant at 12... % 24.74/24.93 --- Run --no-e-matching --enum-inst-sum --full-saturate-quant at 12... % 36.74/37.00 --- Run --finite-model-find --uf-ss=no-minimal at 54... % 37.75/37.93 % SZS status Satisfiable % 37.75/37.93 % SZS output start Model % 37.75/37.93 ( % 37.75/37.93 ; cardinality of $$unsorted is 8 % 37.75/37.93 ; rep: (as @$$unsorted_0 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_1 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_2 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_3 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_4 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_5 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_6 $$unsorted) % 37.75/37.93 ; rep: (as @$$unsorted_7 $$unsorted) % 37.75/37.93 (define-fun tptp.ndr1_0 () Bool true) % 37.75/37.93 (define-fun tptp.c2_0 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC27 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC47 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC45 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC44 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC43 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC41 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC40 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC39 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC36 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC35 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC30 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC28 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC25 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC24 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC23 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC22 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC20 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC18 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC17 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC16 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC15 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC14 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC13 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC11 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC10 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC8 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC7 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC6 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC3 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC2 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC1 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC0 () Bool false) % 37.75/37.93 (define-fun tptp.a1186 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.ndr1_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.c3_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.c8_0 () Bool false) % 37.75/37.93 (define-fun tptp.c4_0 () Bool true) % 37.75/37.93 (define-fun tptp.c7_0 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC42 () Bool true) % 37.75/37.93 (define-fun tptp.c6_0 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC38 () Bool false) % 37.75/37.93 (define-fun tptp.c10_0 () Bool false) % 37.75/37.93 (define-fun tptp.c5_0 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkC26 () Bool true) % 37.75/37.93 (define-fun tptp.c1_0 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC21 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC19 () Bool false) % 37.75/37.93 (define-fun tptp.c9_0 () Bool true) % 37.75/37.93 (define-fun tptp.ssSkC12 () Bool false) % 37.75/37.93 (define-fun tptp.c3_0 () Bool false) % 37.75/37.93 (define-fun tptp.ssSkP11 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.ssSkP10 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.ssSkP9 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.a1165 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c10_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.ssSkP8 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.ssSkP7 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.a1155 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c6_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1153 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.93 (define-fun tptp.c4_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.ssSkP6 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.a1135 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.93 (define-fun tptp.c9_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1131 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.ssSkP5 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.a1118 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c7_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1115 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.ssSkP4 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1089 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c5_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.ssSkP3 (($x1 $$unsorted)) Bool true) % 37.75/37.93 (define-fun tptp.a1079 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c1_1 (($x1 $$unsorted)) Bool (= (as @$$unsorted_0 $$unsorted) $x1)) % 37.75/37.93 (define-fun tptp.ssSkP2 (($x1 $$unsorted)) Bool (not (= (as @$$unsorted_2 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1066 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1062 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1059 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1047 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1040 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1035 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1028 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1022 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1018 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1013 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.93 (define-fun tptp.ssSkP1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a1005 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1003 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.93 (define-fun tptp.c2_1 (($x1 $$unsorted)) Bool (= (as @$$unsorted_2 $$unsorted) $x1)) % 37.75/37.93 (define-fun tptp.a997 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a992 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.ssSkP0 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_1 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 37.75/37.93 (define-fun tptp.a972 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.93 (define-fun tptp.a970 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.93 (define-fun tptp.a966 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.a960 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.93 (define-fun tptp.a1188 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.93 (define-fun tptp.c3_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2))) (not (and (= (as @$$unsorted_7 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2))) (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_7 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))))) % 37.75/37.94 (define-fun tptp.a1187 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1170 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1167 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC46 () Bool false) % 37.75/37.94 (define-fun tptp.a1154 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1143 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c8_1 (($x1 $$unsorted)) Bool (or (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x1))) % 37.75/37.94 (define-fun tptp.a1136 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC37 () Bool false) % 37.75/37.94 (define-fun tptp.a1120 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1087 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1078 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1074 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1072 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1061 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1050 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1033 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1031 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1015 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1007 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a980 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a978 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC5 () Bool true) % 37.75/37.94 (define-fun tptp.a967 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a963 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1181 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.c9_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_7 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))))) % 37.75/37.94 (define-fun tptp.a1179 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c8_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_7 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2)))) % 37.75/37.94 (define-fun tptp.a1177 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c6_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_6 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)))) % 37.75/37.94 (define-fun tptp.a1166 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1157 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c4_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))))) % 37.75/37.94 (define-fun tptp.a1156 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1151 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c2_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)))) % 37.75/37.94 (define-fun tptp.a1146 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1139 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1132 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1119 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1116 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1111 () $$unsorted (as @$$unsorted_7 $$unsorted)) % 37.75/37.94 (define-fun tptp.c10_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2))) (not (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_3 $$unsorted) $x2))) (not (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2))))) % 37.75/37.94 (define-fun tptp.a1091 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c1_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_1 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)) (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_5 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)) (and (= (as @$$unsorted_7 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)) (and (= (as @$$unsorted_4 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)) (and (= (as @$$unsorted_5 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)) (and (= (as @$$unsorted_6 $$unsorted) $x1) (= (as @$$unsorted_4 $$unsorted) $x2)))) % 37.75/37.94 (define-fun tptp.a1090 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.c7_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2))) % 37.75/37.94 (define-fun tptp.a1085 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1076 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1067 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1060 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1058 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1048 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1037 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1036 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1030 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1014 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1011 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1006 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.c5_2 (($x1 $$unsorted) ($x2 $$unsorted)) Bool (or (and (= (as @$$unsorted_0 $$unsorted) $x1) (= (as @$$unsorted_2 $$unsorted) $x2)) (and (= (as @$$unsorted_2 $$unsorted) $x1) (= (as @$$unsorted_0 $$unsorted) $x2)))) % 37.75/37.94 (define-fun tptp.a1004 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a998 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a994 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a993 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a991 () $$unsorted (as @$$unsorted_5 $$unsorted)) % 37.75/37.94 (define-fun tptp.a988 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC48 () Bool false) % 37.75/37.94 (define-fun tptp.a1173 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1171 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1162 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1160 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1144 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1140 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1137 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1133 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1130 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1125 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1123 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1121 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1099 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1095 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1068 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1055 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1046 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1034 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1032 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1024 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1020 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1017 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1016 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a981 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a977 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a973 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a968 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a964 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1128 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1038 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1029 () $$unsorted (as @$$unsorted_5 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1023 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1019 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a961 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1174 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1168 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1164 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1161 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1145 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1141 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1134 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1127 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1126 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1088 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1081 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1075 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1070 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1057 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1056 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1042 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1008 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a986 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC33 () Bool true) % 37.75/37.94 (define-fun tptp.a1163 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1083 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1082 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1069 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1009 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a987 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC32 () Bool false) % 37.75/37.94 (define-fun tptp.ssSkC34 () Bool false) % 37.75/37.94 (define-fun tptp.a1010 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC31 () Bool true) % 37.75/37.94 (define-fun tptp.ssSkC4 () Bool true) % 37.75/37.94 (define-fun tptp.ssSkC49 () Bool false) % 37.75/37.94 (define-fun tptp.ssSkC50 () Bool true) % 37.75/37.94 (define-fun tptp.a1105 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1110 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1138 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1113 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1122 () $$unsorted (as @$$unsorted_3 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1101 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1012 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a976 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a974 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1180 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1152 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC29 () Bool true) % 37.75/37.94 (define-fun tptp.a1178 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1172 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1112 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1104 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1077 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1158 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1092 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1086 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1025 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a989 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1106 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a995 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1142 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1147 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1124 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1117 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1103 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1094 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a983 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a979 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a975 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a969 () $$unsorted (as @$$unsorted_6 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1107 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1114 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1100 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1093 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1041 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1021 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1108 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a962 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC51 () Bool false) % 37.75/37.94 (define-fun tptp.a1183 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1002 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1185 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1184 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1063 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1176 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1045 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1053 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1043 () $$unsorted (as @$$unsorted_4 $$unsorted)) % 37.75/37.94 (define-fun tptp.a982 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1182 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1084 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1049 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1054 () $$unsorted (as @$$unsorted_2 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1044 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1026 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a971 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1159 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1102 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1096 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1039 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1129 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1071 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1000 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.ssSkC9 () Bool true) % 37.75/37.94 (define-fun tptp.a1189 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1150 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1149 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1098 () $$unsorted (as @$$unsorted_1 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1027 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1001 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a984 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1109 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1064 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1065 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1148 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1080 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a965 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a999 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a996 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a985 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1097 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1073 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a1169 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 (define-fun tptp.a990 () $$unsorted (as @$$unsorted_0 $$unsorted)) % 37.75/37.94 ) % 37.75/37.94 % SZS output end Model % 37.75/37.94 % cvc5 exiting %------------------------------------------------------------------------------