WATCH: 0.00 CPU 0.01 WC WATCH: 0.02 CPU 3.02 WC WATCH: 0.02 CPU 6.03 WC [1] 3826 --------------------------SPASS-START----------------------------- Input Problem: 1[0:Inp] || -> $lesseq(f(7),3)*. 2[0:Inp] || $lesseq(f(4),3)* -> . 3[0:Inp] || $int(U) -> $int(f(U))*. 4[0:Inp] || $int(U) -> $lesseq(f($sum(U,1)),f($sum(U,2)))*. This is a first-order Horn problem containing equality. Axiom clauses: 1 Conjecture clauses: 3 Inferences: ISpR=1 ISpL=1 IORe=2 IOFc=2 Reductions: RFRew=1 RBRew=1 RFMRR=1 RBMRR=1 RObv=1 RUnC=1 RTaut=1 RFSub=1 RBSub=1 RCon=1 Extras : No Input Saturation, Precedence Selection, No Splitting, Full Reduction, Ratio: 2147483646, FuncWeight: 1, VarWeight: 1, PrefCon: 1 Precedence: $product > $difference > $sum > f > $to_rat > $to_int > nequal > $$arithuneq > $lesseq > $int > $rat > $real > $less > $greater > $greatereq > $evaleq > $is_int > $is_rat > 2 > 1 > 7 > 3 > 4 Ordering : KBO Processed Problem: Worked Off Clauses: 3[0:Inp] || $int(U) -> $int(f(U))*. Usable Clauses: 1[0:Inp] || -> $lesseq(f(7),3)*. 2[0:Inp] || $lesseq(f(4),3)* -> . 4[0:Inp] || $int(U) -> $lesseq(f($sum(U,1)),f($sum(U,2)))*. Using default external source int Using default external source lesseq_1 Sending question: fof(lesseq_1_Q1,question,( $lesseq(f(4),3) ),unknown,[xdb(limit,number(3))]). WATCH: 1.17 CPU 9.04 WC Sending question: fof(greater_1_Q2,question,( $greater(f(7),3) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q22,question,? [V1,V2] : ( $greater(V1,V2) ),unknown,[xdb(limit,number(3))]). WATCH: 4.16 CPU 12.05 WC Sending question: fof(greater_1_Q64,question,? [V1] : ( $greater(V1,V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(lesseq_1_Q5,question,? [V1] : ( $lesseq(V1,3) ),unknown,[xdb(limit,number(3))]). WATCH: 7.16 CPU 15.06 WC Sending question: fof(greater_1_Q6,question,? [V1] : ( $greater(V1,3) ),unknown,[xdb(limit,number(3))]). Sending question: fof(int_Q3,question,? [V1] : ( $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q4,question,? [V1] : ( $greater(f($sum(V1,1)),f($sum(V1,2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 10.15 CPU 18.07 WC Sending question: fof(greater_1_Q7,question,? [V1] : ( $greater(f($sum(f(V1),1)),f($sum(f(V1),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 13.15 CPU 21.08 WC Sending question: fof(greater_1_Q8,question,? [V1] : ( $greater(f($sum(f(f(V1)),1)),f($sum(f(f(V1)),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q9,question,? [V1] : ( $greater(f($sum(f(f(f(V1))),1)),f($sum(f(f(f(V1))),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 16.14 CPU 24.09 WC Sending question: fof(greater_1_Q10,question,? [V1] : ( $greater(f($sum(f(f(f(f(V1)))),1)),f($sum(f(f(f(f(V1)))),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q11,question,? [V1] : ( $greater(f($sum(f(f(f(f(f(V1))))),1)),f($sum(f(f(f(f(f(V1))))),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 19.14 CPU 27.10 WC Sending question: fof(greater_1_Q12,question,? [V1] : ( $greater(f($sum(f(f(f(f(f(f(V1)))))),1)),f($sum(f(f(f(f(f(f(V1)))))),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q13,question,? [V1] : ( $greater(f($sum(f(f(f(f(f(f(f(V1))))))),1)),f($sum(f(f(f(f(f(f(f(V1))))))),2))) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 22.13 CPU 30.11 WC Sending question: fof(sum_equal_1_Q242,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $greater(V2,V1) & $int($sum(V1,1)) & $sum(V1,2) = V3 & $sum(V1,1) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q255,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $sum(V1,1) = V2 & $sum(V1,1) = V3 & $int($sum(V1,1)) & $greater(V4,V1) ),unknown,[xdb(limit,number(3))]). WATCH: 25.12 CPU 33.12 WC Sending question: fof(sum_equal_1_Q259,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = V2 & $sum(V1,2) = V3 & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) & $greater(V4,V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q265,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = V2 & $greater(V3,V1) & $int($sum(V1,1)) & $sum(V1,1) = V4 & $sum(V1,2) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). WATCH: 28.12 CPU 36.13 WC Sending question: fof(sum_equal_1_Q654,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $sum(V1,1) = V3 & $sum(V1,2) = V4 & $sum(V1,2) = $sum(V1,1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q727,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = V2 & $sum(V1,1) = V3 & $int(V1) & $sum(V1,2) = $sum(V1,1) & $sum(V1,1) = V4 ),unknown,[xdb(limit,number(3))]). WATCH: 31.12 CPU 39.14 WC Sending question: fof(sum_equal_1_Q1297,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $greater(V3,V1) & $int($sum(V1,1)) & $sum(V1,2) = V4 & $sum(V1,2) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1345,question,? [V1,V2,V3,V4] : ( $greater(V1,V2) & $sum(V2,1) = V3 & $sum(V2,1) = V4 & $sum(V2,2) = $sum(V2,1) & $int($sum(V2,1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1369,question,? [V1,V2,V3,V4] : ( $greater(V1,V2) & $sum(V2,2) = V3 & $sum(V2,2) = $sum(V2,1) & $sum(V2,2) = V4 & $int($sum(V2,1)) ),unknown,[xdb(limit,number(3))]). WATCH: 34.11 CPU 42.15 WC Sending question: fof(sum_equal_1_Q1407,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $greater(V2,V1) & $int($sum(V1,1)) & $sum(V1,1) = V3 & $sum(V1,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1443,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $sum(V1,1) = V2 & $sum(V1,2) = V3 & $int(V1) & $sum(V1,1) = V4 ),unknown,[xdb(limit,number(3))]). WATCH: 37.10 CPU 45.16 WC Sending question: fof(sum_equal_1_Q1496,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $sum(V1,1) = V3 & $int(V1) & $sum(V1,2) = $sum(V1,1) & $sum(V1,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1530,question,? [V1,V2,V3,V4] : ( $greater(V1,V2) & $int($sum(V2,1)) & $sum(V2,2) = V3 & $sum(V2,1) = V4 & $sum(V2,2) = $sum(V2,1) ),unknown,[xdb(limit,number(3))]). WATCH: 40.10 CPU 48.17 WC Sending question: fof(sum_equal_1_Q1562,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $sum(V1,1) = V3 & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) & $greater(V4,V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1611,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $sum(V1,2) = V2 & $sum(V1,2) = V3 & $int($sum(V1,1)) & $greater(V4,V1) ),unknown,[xdb(limit,number(3))]). WATCH: 43.09 CPU 51.18 WC Sending question: fof(sum_equal_1_Q1632,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $greater(V3,V1) & $int($sum(V1,1)) & $sum(V1,2) = $sum(V1,1) & $sum(V1,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1662,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = V2 & $sum(V1,1) = V3 & $sum(V1,2) = $sum(V1,1) & $int(V1) & $sum(V1,1) = V4 ),unknown,[xdb(limit,number(3))]). WATCH: 46.10 CPU 54.19 WC Sending question: fof(sum_equal_1_Q1682,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = $sum(V1,1) & $sum(V1,1) = V2 & $int(V1) & $sum(V1,1) = V3 & $sum(V1,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1783,question,? [V1,V2,V3,V4] : ( $sum(V1,2) = V2 & $sum(V1,2) = $sum(V1,1) & $sum(V1,2) = V3 & $int($sum(V1,1)) & $greater(V4,V1) ),unknown,[xdb(limit,number(3))]). WATCH: 49.09 CPU 57.20 WC Sending question: fof(greater_1_Q1803,question,? [V1,V2,V3,V4] : ( $greater(V1,V2) & $int($sum(V2,1)) & $sum(V2,1) = V3 & $sum(V2,2) = $sum(V2,1) & $sum(V2,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1831,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $sum(V1,2) = V3 & $sum(V1,2) = $sum(V1,1) & $int(V1) & $sum(V1,1) = V4 ),unknown,[xdb(limit,number(3))]). WATCH: 52.08 CPU 60.21 WC Sending question: fof(sum_equal_1_Q1855,question,? [V1,V2,V3,V4] : ( $sum(V1,1) = V2 & $int(V1) & $sum(V1,2) = $sum(V1,1) & $sum(V1,1) = V3 & $sum(V1,2) = V4 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q834,question,? [V1,V2,V3] : ( $sum(V1,1) = 4 & $sum(V1,2) = V2 & $sum(V1,2) = $sum(V1,1) & $int(V1) & $sum(V1,1) = V3 ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q79,question,? [V1,V2] : ( f(V1) = $sum(f(V2),1) & $int(V2) & V1 = $sum(f(V2),2) & $greater($sum(f(V2),1),$sum(f(V2),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 55.07 CPU 63.22 WC Sending question: fof(equal_sum_1_Q80,question,? [V1,V2] : ( V1 = $sum(f(V2),1) & $int(V2) & f(V1) = $sum(f(V2),2) & $greater($sum(f(V2),2),$sum(f(V2),2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q161,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $int(f(f(V1))) & $sum(f(V1),1) = V1 & $greater($sum(f(V1),2),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 58.07 CPU 66.23 WC Sending question: fof(sum_equal_1_Q258,question,? [V1] : ( $sum(V1,2) = $sum(V1,1) & f($sum(V1,2)) = $sum(V1,1) & $int($sum(V1,1)) & $greater($sum(V1,1),V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q264,question,? [V1] : ( $sum(V1,2) = $sum(V1,1) & f($sum(V1,1)) = $sum(V1,2) & $int($sum(V1,1)) & $greater($sum(V1,2),V1) ),unknown,[xdb(limit,number(3))]). WATCH: 61.06 CPU 69.24 WC Sending question: fof(greater_1_Q291,question,? [V1] : ( $greater(f(V1),f(V1)) & $sum($sum(f(f(V1)),2),1) = V1 & $sum(f(f(V1)),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q325,question,? [V1,V2,V3] : ( $sum($sum(V1,2),1) = f(f(V2)) & $sum(V1,2) = f(V2) & $int(V2) & $greater(V3,$sum($sum(V1,2),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 64.06 CPU 72.24 WC Sending question: fof(greater_1_Q326,question,? [V1,V2,V3] : ( $greater(V1,$sum(f(f(V2)),1)) & $int(V2) & V3 = $sum(f(f(V2)),2) & f(V3) = $sum(f(f(V2)),1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q328,question,? [V1,V2,V3] : ( $sum(f(f(V1)),1) = f(V2) & $greater($sum(f(f(V1)),1),V3) & $sum(f(f(V1)),2) = V2 & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 67.05 CPU 75.25 WC Sending question: fof(equal_sum_1_Q329,question,? [V1,V2,V3] : ( V1 = $sum(f(f(V2)),1) & f(V1) = $sum(f(f(V2)),2) & $greater($sum(f(f(V2)),2),V3) & $int(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q331,question,? [V1,V2,V3] : ( V1 = $sum(f(f(V2)),1) & f(V1) = $sum(f(f(V2)),2) & $greater(V3,$sum(f(f(V2)),2)) & $int(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 70.04 CPU 78.26 WC Sending question: fof(sum_equal_1_Q398,question,? [V1,V2,V3] : ( $sum(f(f(V1)),1) = f(V2) & $sum(f(f(V1)),2) = V2 & $int(V1) & $greater(V3,$sum(f(f(V1)),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q414,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $sum(f(V1),1) = V1 & $int(f(f(V1))) & $greater(f(V1),$sum(f(V1),2)) ),unknown,[xdb(limit,number(3))]). WATCH: 73.05 CPU 81.28 WC Sending question: fof(sum_equal_1_Q419,question,? [V1] : ( $sum(f(f(V1)),1) = V1 & $sum(f(V1),2) = f(V1) & $greater(f(f(V1)),$sum(f(V1),2)) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q437,question,? [V1,V2,V3] : ( $greater(V1,$sum(f(f(V2)),2)) & f(V3) = $sum(f(f(V2)),2) & V3 = $sum(f(f(V2)),1) & $int(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q445,question,? [V1,V2] : ( $greater(V1,f(V2)) & $int(V2) & $sum(f(f(V2)),1) = f(V2) & $sum($sum(f(f(V2)),1),2) = f(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 76.04 CPU 84.29 WC Sending question: fof(sum_equal_1_Q446,question,? [V1,V2] : ( $sum($sum(f(f(V1)),1),2) = f(V1) & $greater(f(V1),V2) & $int(V1) & $sum(f(f(V1)),1) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q506,question,? [V1,V2,V3] : ( $sum(f(f(V1)),1) = f(V1) & $sum(V2,2) = V1 & $int(V3) & $greater(f(f(V3)),$sum(f(f(V1)),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 79.04 CPU 87.30 WC Sending question: fof(equal_sum_1_Q507,question,? [V1,V2] : ( V1 = $sum($sum(f(f(V2)),2),1) & $greater(f(V2),f(V2)) & $sum(f(f(V2)),2) = f(V2) & $int(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q509,question,? [V1,V2,V3] : ( $greater($sum(f(f(V1)),2),f(f(V2))) & $sum(f(f(V1)),2) = f(V1) & $sum(V3,1) = V1 & $int(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 82.04 CPU 90.32 WC Sending question: fof(sum_equal_1_Q549,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $sum($sum(f(V1),2),1) = V1 & $int(f(f(V1))) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q587,question,? [V1,V2] : ( f(V1) = $sum($sum(V2,1),2) & f(f(V1)) = $sum(V2,1) & $int(V1) & $greater($sum(V2,1),$sum(V2,1)) ),unknown,[xdb(limit,number(3))]). WATCH: 85.05 CPU 93.33 WC Sending question: fof(equal_sum_1_Q718,question,? [V1] : ( f($sum(V1,2)) = $sum(V1,1) & $int(V1) & $sum(V1,2) = $sum(V1,1) & $greater($sum(V1,1),$sum(V1,1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q723,question,? [V1] : ( f($sum(V1,1)) = $sum(V1,2) & $int(V1) & $sum(V1,2) = $sum(V1,1) & $greater($sum(V1,2),$sum(V1,2)) ),unknown,[xdb(limit,number(3))]). WATCH: 88.05 CPU 96.34 WC Sending question: fof(sum_equal_1_Q774,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $int(V1) & $sum(V2,1) = V1 & $greater($sum(f(f(V1)),2),f(f(V1))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1128,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $greater(f(V1),V2) & $sum($sum(f(f(V1)),2),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 91.04 CPU 99.36 WC Sending question: fof(greater_1_Q1129,question,? [V1,V2] : ( $greater(V1,f(f(V2))) & $int(V2) & $sum(f(f(V2)),2) = f(V2) & $sum($sum(f(f(V2)),2),1) = V2 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1133,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $sum($sum(f(V1),2),1) = V1 & $int(V1) & $greater(f(V1),$sum(f(V1),2)) ),unknown,[xdb(limit,number(3))]). WATCH: 94.04 CPU 102.37 WC Sending question: fof(greater_1_Q1147,question,? [V1,V2] : ( $greater(f(f(V1)),$sum(V2,2)) & $int(V1) & f(f(V1)) = $sum(V2,2) & $sum($sum(V2,2),1) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1148,question,? [V1,V2] : ( $sum(V1,2) = f(f(V2)) & $int(V2) & f(V2) = $sum($sum(V1,2),1) & $greater($sum(V1,2),$sum(V1,2)) ),unknown,[xdb(limit,number(3))]). WATCH: 97.04 CPU 105.38 WC Sending question: fof(sum_equal_1_Q1168,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $sum(f(V1),1) = V1 & $int(V1) & $greater(f(V1),$sum($sum(f(V1),2),2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1170,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $sum(V2,1) = V1 & $int(V1) & $greater(V2,$sum($sum(f(f(V1)),2),2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1212,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $greater($sum(f(V1),2),f(V1)) & $int(V1) & $sum($sum(f(V1),2),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 100.04 CPU 108.39 WC Sending question: fof(sum_equal_1_Q1217,question,? [V1,V2] : ( $sum(f(f(V1)),1) = V1 & $greater($sum(f(f(V1)),2),V2) & $sum(f(f(V1)),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1227,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $int(V2) & $sum(f(V2),1) = V1 & $greater($sum(f(f(V1)),2),f(V2)) ),unknown,[xdb(limit,number(3))]). WATCH: 103.04 CPU 111.41 WC Sending question: fof(equal_sum_1_Q1240,question,? [V1,V2] : ( f(f(V1)) = $sum($sum(V2,1),2) & $int(V1) & $sum(V2,1) = f(V1) & $greater($sum($sum(V2,1),2),V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1248,question,? [V1,V2] : ( $sum(f(f(V1)),1) = V1 & $greater($sum(f(f(V1)),2),f(f(V1))) & $sum(V2,2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 106.03 CPU 114.42 WC Sending question: fof(sum_equal_1_Q1249,question,? [V1,V2] : ( $sum(f(f(V1)),1) = V1 & $greater($sum(V2,2),f(f(V1))) & $sum(f(f(V1)),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q1254,question,? [V1,V2] : ( f(V1) = $sum($sum(V2,2),1) & $int(V1) & $sum(V2,2) = f(f(V1)) & $greater($sum(V2,2),f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 109.04 CPU 117.43 WC Sending question: fof(sum_equal_1_Q1262,question,? [V1,V2] : ( $sum(V1,2) = f(f(f(V2))) & f(f(V2)) = $sum(V1,1) & $int(V2) & $greater($sum(V1,2),$sum(V1,1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1264,question,? [V1,V2,V3] : ( $greater($sum(V1,2),f(f(f(V2)))) & $int(V2) & $sum(f(f(f(V2))),1) = V3 & f(V3) = $sum(V1,2) ),unknown,[xdb(limit,number(3))]). WATCH: 112.05 CPU 120.45 WC Sending question: fof(sum_equal_1_Q1280,question,? [V1,V2] : ( $sum(f(f(V1)),1) = V1 & f(V1) = $sum(V2,2) & $int($sum(V2,2)) & $greater($sum(V2,2),f(f(V1))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1300,question,? [V1,V2] : ( $sum($sum(f(f(V1)),2),1) = V1 & $greater(f(f(V1)),V2) & $int(V1) & $sum(f(f(V1)),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 115.04 CPU 123.46 WC Sending question: fof(sum_equal_1_Q1307,question,? [V1,V2] : ( $sum(f(V1),2) = f(f(V2)) & $int(V2) & $sum($sum(f(V1),2),1) = V1 & $greater(f(f(V2)),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1367,question,? [V1,V2] : ( $greater($sum(f(V1),2),f(f(f(V2)))) & $int(V2) & $sum(f(V1),1) = V1 & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 118.04 CPU 126.47 WC Sending question: fof(greater_1_Q1397,question,? [V1] : ( $greater(f(V1),f(V1)) & $sum($sum(f(f(V1)),1),2) = V1 & $sum(f(f(V1)),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1441,question,? [V1,V2] : ( $sum(f(f(V1)),1) = f(V1) & $sum(V2,2) = V1 & $int(V1) & $greater($sum(f(f(V1)),1),f(f(V1))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1448,question,? [V1] : ( $greater(f(V1),$sum(f(V1),1)) & $sum($sum(f(V1),1),2) = V1 & $sum(f(V1),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 121.03 CPU 129.48 WC Sending question: fof(greater_1_Q1458,question,? [V1,V2,V3] : ( $greater(V1,f(f(f(V2)))) & $int(V2) & f(f(V2)) = $sum($sum(V3,2),1) & $sum(V3,2) = f(f(V2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1466,question,? [V1] : ( $sum(f(f(V1)),1) = V1 & $sum(f(V1),2) = f(V1) & $greater(f(V1),$sum(f(V1),2)) & $int(f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 124.02 CPU 132.49 WC Sending question: fof(sum_equal_1_Q1469,question,? [V1] : ( $sum($sum(f(V1),2),1) = V1 & $greater(f(V1),f(f(V1))) & $int(f(V1)) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1474,question,? [V1] : ( $sum($sum(f(V1),2),1) = V1 & $greater(f(f(V1)),f(V1)) & $int(f(V1)) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 127.01 CPU 135.50 WC Sending question: fof(greater_1_Q1492,question,? [V1,V2] : ( $greater(f(V1),f(V2)) & $sum($sum(f(f(V1)),2),1) = V2 & $sum(f(f(V1)),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1515,question,? [V1] : ( $greater($sum(f(V1),1),f(V1)) & $sum($sum(f(V1),1),2) = V1 & $sum(f(V1),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 130.00 CPU 138.51 WC Sending question: fof(sum_equal_1_Q1525,question,? [V1,V2] : ( $sum($sum(f(f(V1)),2),1) = V2 & $sum(f(f(V1)),2) = f(V1) & $int(V1) & $greater(f(V2),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1527,question,? [V1] : ( $sum(f(f(V1)),1) = f(V1) & $sum(f(V1),2) = V1 & $int(V1) & $greater($sum(f(f(V1)),1),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 133.00 CPU 141.52 WC Sending question: fof(sum_equal_1_Q1567,question,? [V1,V2] : ( $sum(f(f(V1)),1) = f(V1) & $sum(V2,2) = V1 & $int(V1) & $greater(f(f(V1)),$sum(f(f(V1)),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1572,question,? [V1] : ( $sum(f(f(V1)),1) = f(V1) & $sum(f(V1),2) = V1 & $int(V1) & $greater(f(V1),$sum(f(f(V1)),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 136.00 CPU 144.53 WC Sending question: fof(sum_equal_1_Q1730,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $int(f(f(V1))) & $sum(f(V1),2) = V1 & $greater($sum(f(V1),1),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q1738,question,? [V1] : ( f($sum(V1,1)) = $sum(V1,1) & $greater($sum(V1,1),V1) & $int($sum(V1,1)) & $sum(V1,2) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). WATCH: 138.99 CPU 147.54 WC Sending question: fof(sum_equal_1_Q1823,question,? [V1] : ( $sum($sum(f(V1),1),2) = V1 & $sum(f(V1),1) = f(V1) & $int(f(V1)) & $greater(f(V1),f(f(V1))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q1848,question,? [V1] : ( $greater(f(f(V1)),f(V1)) & $sum(f(V1),1) = f(V1) & $sum($sum(f(V1),1),2) = V1 & $int(f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 141.99 CPU 150.55 WC Sending question: fof(sum_equal_1_Q1919,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $int(f(f(V1))) & $sum(f(V1),2) = V1 & $greater(f(V1),$sum(f(V1),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q1959,question,? [V1] : ( $sum($sum(f(V1),1),2) = V1 & $greater(f(V1),f(V1)) & $sum(f(V1),1) = f(V1) & $int(f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 144.98 CPU 153.55 WC Sending question: fof(greater_1_Q2007,question,? [V1,V2] : ( $greater($sum(f(V1),1),$sum(f(V1),1)) & $int(V1) & V2 = $sum(f(V1),2) & f(V2) = $sum(f(V1),1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2043,question,? [V1,V2] : ( $greater($sum(f(V1),2),$sum(f(V1),2)) & $int(V1) & f(V2) = $sum(f(V1),2) & V2 = $sum(f(V1),1) ),unknown,[xdb(limit,number(3))]). WATCH: 147.98 CPU 156.56 WC Sending question: fof(greater_1_Q2082,question,? [V1] : ( $greater($sum(f(V1),2),f(V1)) & $int(f(f(V1))) & $sum(f(V1),1) = V1 & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2101,question,? [V1] : ( $greater($sum(V1,1),V1) & f($sum(V1,2)) = $sum(V1,1) & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) ),unknown,[xdb(limit,number(3))]). WATCH: 150.97 CPU 159.57 WC Sending question: fof(sum_equal_1_Q2110,question,? [V1,V2,V3] : ( $sum(f(V1),2) = V1 & $sum(f(V2),2) = V3 & $sum(f(V1),2) = 4 & $sum(f(V1),2) = V2 ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2119,question,? [V1] : ( $greater($sum(V1,2),V1) & f($sum(V1,1)) = $sum(V1,2) & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) ),unknown,[xdb(limit,number(3))]). WATCH: 153.96 CPU 162.58 WC Sending question: fof(sum_equal_1_Q2135,question,? [V1] : ( $sum(f(f(V1)),2) = f(V1) & $sum($sum(f(f(V1)),2),1) = V1 & $int(V1) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2144,question,? [V1,V2,V3] : ( $greater(V1,$sum($sum(V2,2),1)) & $int(V3) & $sum(V2,2) = f(V3) & $sum($sum(V2,2),1) = f(f(V3)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q2159,question,? [V1,V2,V3] : ( f(V1) = $sum(f(f(V2)),1) & $int(V2) & V1 = $sum(f(f(V2)),2) & $greater(V3,$sum(f(f(V2)),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 156.97 CPU 165.59 WC Sending question: fof(sum_equal_1_Q2165,question,? [V1,V2,V3] : ( $sum(f(f(V1)),2) = V2 & $greater($sum(f(f(V1)),1),V3) & $sum(f(f(V1)),1) = f(V2) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2196,question,? [V1] : ( $greater(f(f(V1)),$sum(f(V1),1)) & $int(V1) & $sum(f(f(V1)),2) = V1 & $sum(f(V1),1) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 159.96 CPU 168.60 WC Sending question: fof(greater_1_Q2202,question,? [V1,V2,V3] : ( $greater($sum(f(f(V1)),2),V2) & f(V3) = $sum(f(f(V1)),2) & V3 = $sum(f(f(V1)),1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q2213,question,? [V1,V2,V3] : ( f(V1) = $sum(f(f(V2)),2) & $greater(V3,$sum(f(f(V2)),2)) & V1 = $sum(f(f(V2)),1) & $int(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 162.96 CPU 171.61 WC Sending question: fof(greater_1_Q2231,question,? [V1,V2,V3] : ( $greater(V1,$sum(f(f(V2)),1)) & $sum(f(f(V2)),2) = V3 & $sum(f(f(V2)),1) = f(V3) & $int(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2243,question,? [V1,V2] : ( $sum($sum(f(f(V1)),1),2) = V1 & $greater(f(f(V1)),V2) & $int(V1) & $sum(f(f(V1)),1) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 165.96 CPU 174.62 WC Sending question: fof(greater_1_Q2246,question,? [V1] : ( $greater(f(V1),$sum(f(V1),2)) & $sum(f(V1),1) = V1 & $int(f(f(V1))) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2258,question,? [V1] : ( $greater(f(f(V1)),$sum(f(V1),2)) & $sum(f(V1),2) = f(V1) & $int(V1) & $sum(f(f(V1)),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 168.96 CPU 177.63 WC Sending question: fof(sum_equal_1_Q2324,question,? [V1,V2] : ( $sum($sum(f(f(V1)),1),2) = f(V1) & $int(V1) & $sum(f(f(V1)),1) = f(V1) & $greater(V2,f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2333,question,? [V1,V2] : ( $sum(f(f(V1)),1) = f(V1) & $greater(f(V1),V2) & $int(V1) & $sum($sum(f(f(V1)),1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 171.95 CPU 180.64 WC Sending question: fof(greater_1_Q2334,question,? [V1,V2,V3] : ( $greater(f(f(V1)),$sum(f(f(V2)),1)) & $sum(V3,2) = V2 & $sum(f(f(V2)),1) = f(V2) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2342,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $greater(f(V1),f(V1)) & V2 = $sum($sum(f(f(V1)),2),1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 174.94 CPU 183.65 WC Sending question: fof(sum_equal_1_Q2352,question,? [V1,V2,V3] : ( $sum(V1,1) = V2 & $sum(f(f(V2)),2) = f(V2) & $int(V3) & $greater($sum(f(f(V2)),2),f(f(V3))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2375,question,? [V1] : ( $greater(f(V1),f(V1)) & $sum($sum(f(V1),2),1) = V1 & $sum(f(V1),2) = f(V1) & $int(f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 177.94 CPU 186.66 WC Sending question: fof(greater_1_Q2384,question,? [V1,V2] : ( $greater($sum(V1,1),$sum(V1,1)) & $int(V2) & f(f(V2)) = $sum(V1,1) & f(V2) = $sum($sum(V1,1),2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2413,question,? [V1] : ( $greater($sum(V1,1),$sum(V1,1)) & $int(V1) & $sum(V1,2) = $sum(V1,1) & f($sum(V1,2)) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). WATCH: 180.93 CPU 189.67 WC Sending question: fof(sum_equal_1_Q2439,question,? [V1] : ( $sum(f(f(V1)),2) = V1 & $sum(f(V1),1) = f(V1) & $int(f(V1)) & $greater(f(V1),$sum(f(V1),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2451,question,? [V1] : ( $greater($sum(V1,2),$sum(V1,2)) & $int(V1) & $sum(V1,2) = $sum(V1,1) & f($sum(V1,1)) = $sum(V1,2) ),unknown,[xdb(limit,number(3))]). WATCH: 183.93 CPU 192.68 WC Sending question: fof(greater_1_Q2486,question,? [V1,V2] : ( $greater($sum(f(f(V1)),2),f(f(V1))) & $int(V1) & $sum(V2,1) = V1 & $sum(f(f(V1)),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2489,question,? [V1,V2] : ( $sum($sum(f(f(V1)),2),1) = f(V1) & $greater(f(V1),V2) & $sum(f(f(V1)),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2490,question,? [V1,V2] : ( $sum($sum(f(f(V1)),2),1) = V1 & $int(V1) & $sum(f(f(V1)),2) = f(V1) & $greater(V2,f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 186.92 CPU 195.69 WC Sending question: fof(greater_1_Q2491,question,? [V1] : ( $greater(f(V1),$sum(f(V1),2)) & $sum($sum(f(V1),2),1) = V1 & $sum(f(V1),2) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2493,question,? [V1,V2] : ( $sum($sum(V1,2),1) = f(V2) & $int(V2) & f(f(V2)) = $sum(V1,2) & $greater(f(f(V2)),$sum(V1,2)) ),unknown,[xdb(limit,number(3))]). WATCH: 189.92 CPU 198.71 WC Sending question: fof(greater_1_Q2499,question,? [V1,V2] : ( $greater($sum(V1,2),$sum(V1,2)) & $int(V2) & f(V2) = $sum($sum(V1,2),1) & $sum(V1,2) = f(f(V2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2504,question,? [V1] : ( $greater(f(V1),$sum($sum(f(V1),2),2)) & $sum(f(V1),1) = V1 & $int(V1) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 192.92 CPU 201.72 WC Sending question: fof(greater_1_Q2511,question,? [V1,V2,V3] : ( $greater(f(f(f(f(V1)))),f(V2)) & $int(V1) & $sum(V3,1) = f(f(f(V1))) & $sum(f(V2),2) = V2 ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2517,question,? [V1,V2,V3] : ( $greater(f(f(f(f(V1)))),f(V2)) & $int(V1) & $sum(f(V2),1) = V2 & $sum(V3,2) = f(f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 195.92 CPU 204.73 WC Sending question: fof(greater_1_Q2519,question,? [V1,V2,V3] : ( $greater(f(V1),f(f(f(f(V2))))) & $int(V2) & $sum(f(V1),1) = V1 & $sum(V3,2) = f(f(f(V2))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2529,question,? [V1,V2] : ( $greater(V1,$sum($sum(f(f(V2)),2),2)) & $sum(V1,1) = V2 & $int(V2) & $sum(f(f(V2)),2) = f(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 198.93 CPU 207.74 WC Sending question: fof(sum_equal_1_Q2547,question,? [V1] : ( $sum($sum(f(V1),2),1) = V1 & $greater($sum(f(V1),2),f(V1)) & $int(V1) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2578,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $greater($sum(f(f(V1)),2),V2) & $sum(f(f(V1)),1) = V1 & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 201.92 CPU 210.76 WC Sending question: fof(greater_1_Q2600,question,? [V1,V2] : ( $greater($sum(f(f(V1)),2),f(V2)) & $int(V2) & $sum(f(V2),1) = V1 & $sum(f(f(V1)),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2623,question,? [V1,V2] : ( $greater($sum($sum(V1,1),2),V1) & $int(V2) & $sum(V1,1) = f(V2) & f(f(V2)) = $sum($sum(V1,1),2) ),unknown,[xdb(limit,number(3))]). WATCH: 204.92 CPU 213.77 WC Sending question: fof(sum_equal_1_Q2633,question,? [V1] : ( $sum(f(f(V1)),2) = f(V1) & $sum(f(V1),1) = V1 & $int(V1) & $greater(f(V1),$sum(f(f(V1)),2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2641,question,? [V1,V2] : ( $sum(V1,2) = f(V2) & $greater($sum(f(f(V2)),2),f(f(V2))) & $sum(f(f(V2)),1) = V2 & $int(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 207.92 CPU 216.78 WC Sending question: fof(sum_equal_1_Q2642,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $greater($sum(V2,2),f(f(V1))) & $sum(f(f(V1)),1) = V1 & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2643,question,? [V1,V2] : ( $greater($sum(V1,2),f(f(V2))) & $int(V2) & $sum(V1,2) = f(f(V2)) & f(V2) = $sum($sum(V1,2),1) ),unknown,[xdb(limit,number(3))]). WATCH: 210.91 CPU 219.79 WC Sending question: fof(greater_1_Q2644,question,? [V1,V2] : ( $greater($sum(V1,2),$sum(V1,1)) & $int(V2) & f(f(V2)) = $sum(V1,1) & $sum(V1,2) = f(f(f(V2))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q2645,question,? [V1,V2,V3] : ( f(V1) = $sum(V2,2) & $int(V3) & $sum(f(f(f(V3))),1) = V1 & $greater($sum(V2,2),f(f(f(V3)))) ),unknown,[xdb(limit,number(3))]). WATCH: 213.91 CPU 222.80 WC Sending question: fof(greater_1_Q2646,question,? [V1,V2] : ( $greater($sum(V1,2),f(f(V2))) & f(V2) = $sum(V1,2) & $sum(f(f(V2)),1) = V2 & $int($sum(V1,2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2647,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $greater(f(f(V1)),V2) & $int(V1) & $sum($sum(f(f(V1)),2),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 216.90 CPU 225.81 WC Sending question: fof(greater_1_Q2648,question,? [V1,V2] : ( $greater(f(f(V1)),f(V2)) & $int(V1) & $sum($sum(f(V2),2),1) = V2 & $sum(f(V2),2) = f(f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2649,question,? [V1,V2] : ( $sum(f(V1),2) = f(V1) & $int(V2) & $sum(f(V1),1) = V1 & $greater($sum(f(V1),2),f(f(f(V2)))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2651,question,? [V1] : ( $sum(f(f(V1)),1) = f(V1) & $sum($sum(f(f(V1)),1),2) = V1 & $int(V1) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 219.90 CPU 228.82 WC Sending question: fof(greater_1_Q2662,question,? [V1,V2] : ( $greater($sum(f(f(V1)),1),f(f(V1))) & $sum(V2,2) = V1 & $sum(f(f(V1)),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2671,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $sum($sum(f(V1),1),2) = V1 & $int(V1) & $greater(f(V1),$sum(f(V1),1)) ),unknown,[xdb(limit,number(3))]). WATCH: 222.90 CPU 231.83 WC Sending question: fof(sum_equal_1_Q2675,question,? [V1,V2,V3] : ( $sum(V1,2) = f(f(V2)) & $int(V2) & f(f(V2)) = $sum($sum(V1,2),1) & $greater(V3,f(f(f(V2)))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2678,question,? [V1] : ( $greater(f(V1),$sum(f(V1),2)) & $sum(f(V1),2) = f(V1) & $int(f(V1)) & $sum(f(f(V1)),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 225.90 CPU 234.84 WC Sending question: fof(sum_equal_1_Q2681,question,? [V1,V2] : ( $sum($sum(V1,1),2) = f(V2) & $int(V2) & $sum(V1,1) = f(f(V2)) & $greater($sum(V1,1),f(f(V2))) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2687,question,? [V1,V2] : ( $sum(f(V1),1) = f(f(V2)) & $int(V2) & $sum($sum(f(V1),1),2) = V1 & $greater(f(f(V2)),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 228.89 CPU 237.85 WC Sending question: fof(sum_equal_1_Q2695,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $greater(f(V1),f(f(V1))) & $int(f(V1)) & $sum($sum(f(V1),2),1) = V1 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2700,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $greater(f(f(V1)),f(V1)) & $int(f(V1)) & $sum($sum(f(V1),2),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 231.89 CPU 240.86 WC Sending question: fof(sum_equal_1_Q2715,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & $sum($sum(f(f(V1)),2),1) = V2 & $int(V1) & $greater(f(V1),f(V2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2726,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $sum($sum(f(V1),1),2) = V1 & $int(V1) & $greater($sum(f(V1),1),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 234.88 CPU 243.87 WC Sending question: fof(greater_1_Q2729,question,? [V1,V2] : ( $greater(f(V1),f(V2)) & $sum(f(f(V2)),2) = f(V2) & $sum($sum(f(f(V2)),2),1) = V1 & $int(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2753,question,? [V1] : ( $greater($sum(f(f(V1)),1),f(V1)) & $sum(f(V1),2) = V1 & $sum(f(f(V1)),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 237.88 CPU 246.88 WC Sending question: fof(greater_1_Q2773,question,? [V1,V2] : ( $greater(f(V1),$sum(f(V1),1)) & $int(V1) & V2 = $sum($sum(f(V1),1),2) & $sum(f(V1),1) = f(V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2775,question,? [V1,V2] : ( $greater(f(f(V1)),$sum(f(f(V1)),1)) & $sum(V2,2) = V1 & $sum(f(f(V1)),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 240.87 CPU 249.89 WC Sending question: fof(greater_1_Q2780,question,? [V1,V2] : ( $greater($sum(f(V1),1),f(V1)) & $int(V1) & $sum(f(V1),1) = f(V2) & V2 = $sum($sum(f(V1),1),2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q2788,question,? [V1] : ( $greater(f(V1),$sum(f(f(V1)),1)) & $sum(f(V1),2) = V1 & $sum(f(f(V1)),1) = f(V1) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 243.87 CPU 252.90 WC Sending question: fof(greater_1_Q2802,question,? [V1] : ( $greater($sum(f(V1),1),f(V1)) & $int(f(f(V1))) & $sum(f(V1),2) = V1 & $sum(f(V1),1) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2805,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $sum(f(V1),1) = V1 & $int(V1) & $greater($sum($sum(f(V1),2),2),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 246.86 CPU 255.91 WC Sending question: fof(sum_equal_1_Q2807,question,? [V1,V2] : ( $sum(f(f(V1)),2) = f(V1) & V1 = $sum(V2,1) & $int(V1) & $greater($sum($sum(f(f(V1)),2),2),V2) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2833,question,? [V1] : ( $sum(V1,2) = $sum(V1,1) & $greater($sum(V1,1),V1) & $int($sum(V1,1)) & f($sum(V1,1)) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). WATCH: 249.87 CPU 258.92 WC Sending question: fof(greater_1_Q2855,question,? [V1] : ( $greater(f(V1),f(f(V1))) & $sum(f(V1),1) = f(V1) & $sum($sum(f(V1),1),2) = V1 & $int(f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2888,question,? [V1] : ( $sum($sum(f(V1),1),2) = V1 & $sum(f(V1),1) = f(V1) & $int(f(V1)) & $greater(f(f(V1)),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 252.87 CPU 261.93 WC Sending question: fof(greater_1_Q2910,question,? [V1] : ( $greater(f(V1),$sum(f(V1),1)) & $int(f(f(V1))) & $sum(f(V1),2) = V1 & $sum(f(V1),1) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2922,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $greater(f(V1),f(V1)) & $sum($sum(f(V1),1),2) = V1 & $int(f(f(V1))) ),unknown,[xdb(limit,number(3))]). WATCH: 255.86 CPU 264.94 WC Sending question: fof(equal_sum_1_Q2936,question,? [V1,V2] : ( V1 = $sum(f(V2),2) & $int(V2) & f(V1) = $sum(f(V2),1) & $greater($sum(f(V2),1),$sum(f(V2),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q2942,question,? [V1,V2] : ( f(V1) = $sum(f(V2),2) & $int(V2) & V1 = $sum(f(V2),1) & $greater($sum(f(V2),2),$sum(f(V2),2)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2958,question,? [V1] : ( $sum(f(V1),1) = V1 & $int(f(f(V1))) & $sum(f(V1),2) = f(V1) & $greater($sum(f(V1),2),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 258.85 CPU 267.95 WC Sending question: fof(sum_equal_1_Q2965,question,? [V1,V2] : ( $sum(V1,1) = V2 & $int($sum(V1,1)) & $sum(V1,1) = f(V2) & $sum($sum(V1,1),2) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q2970,question,? [V1] : ( f($sum(V1,2)) = $sum(V1,1) & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) & $greater($sum(V1,1),V1) ),unknown,[xdb(limit,number(3))]). WATCH: 261.85 CPU 270.96 WC Sending question: fof(sum_equal_1_Q2992,question,? [V1,V2,V3] : ( $sum(f(V1),2) = V2 & $sum(f(V3),2) = V3 & $sum(f(V3),2) = 4 & $sum(f(V3),2) = V1 ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q2993,question,? [V1,V2] : ( $sum(V1,2) = $sum(V1,1) & $int(V2) & f(f(f(f(f(f(f(V2))))))) = $sum(V1,2) & $greater(V1,V1) ),unknown,[xdb(limit,number(3))]). WATCH: 264.84 CPU 273.97 WC Sending question: fof(equal_sum_1_Q3005,question,? [V1] : ( f($sum(V1,1)) = $sum(V1,2) & $sum(V1,2) = $sum(V1,1) & $int($sum(V1,1)) & $greater($sum(V1,2),V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3042,question,? [V1] : ( $sum($sum(f(f(V1)),2),1) = V1 & $sum(f(f(V1)),2) = f(V1) & $int(V1) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). WATCH: 267.83 CPU 276.98 WC Sending question: fof(equal_sum_1_Q3049,question,? [V1,V2] : ( f(V1) = $sum(V2,2) & $sum(f(f(V1)),2) = $sum($sum(V2,2),1) & $int(V1) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q3051,question,? [V1,V2] : ( $greater(f(V1),f(V1)) & $sum($sum(V2,2),2) = $sum(f(f(V1)),1) & f(V1) = $sum(V2,2) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 270.83 CPU 280.00 WC Sending question: fof(sum_equal_1_Q3056,question,? [V1,V2,V3] : ( $sum(V1,2) = f(V2) & $sum($sum(V1,2),1) = f(f(V2)) & $int(V2) & $greater(V3,$sum($sum(V1,2),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3066,question,? [V1,V2] : ( $sum($sum(V1,1),2) = $sum(V1,1) & $int($sum(V1,1)) & $sum(V1,1) = f(V2) & $sum(V1,1) = V2 ),unknown,[xdb(limit,number(3))]). WATCH: 273.83 CPU 283.00 WC Sending question: fof(equal_sum_1_Q3069,question,? [V1,V2,V3] : ( V1 = $sum(f(f(V2)),2) & $int(V2) & f(V1) = $sum(f(f(V2)),1) & $greater(V3,$sum(f(f(V2)),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q3077,question,? [V1,V2,V3] : ( $greater($sum(f(f(V1)),1),V2) & $sum(f(f(V1)),2) = V3 & $sum(f(f(V1)),1) = f(V3) & $int(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 276.83 CPU 286.02 WC Sending question: fof(sum_equal_1_Q3105,question,? [V1] : ( $sum(f(V1),1) = f(V1) & $int(V1) & $sum(f(f(V1)),2) = V1 & $greater(f(f(V1)),$sum(f(V1),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3140,question,? [V1,V2] : ( $sum($sum(V1,1),2) = $sum(f(f(V2)),1) & $int(V2) & $greater(f(V2),f(V2)) & f(V2) = $sum(V1,1) ),unknown,[xdb(limit,number(3))]). WATCH: 279.83 CPU 289.03 WC Sending question: fof(sum_equal_1_Q3142,question,? [V1,V2] : ( $sum(f(f(V1)),2) = $sum($sum(V2,1),1) & $int(V1) & $greater(f(V1),f(V1)) & f(V1) = $sum(V2,1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(equal_sum_1_Q3144,question,? [V1,V2,V3] : ( f(V1) = $sum(f(f(V2)),2) & $greater($sum(f(f(V2)),2),V3) & V1 = $sum(f(f(V2)),1) & $int(V2) ),unknown,[xdb(limit,number(3))]). WATCH: 282.82 CPU 292.05 WC Sending question: fof(sum_equal_1_Q3179,question,? [V1,V2,V3] : ( $sum(f(f(V1)),2) = V2 & $sum(f(f(V1)),1) = f(V2) & $int(V1) & $greater(V3,$sum(f(f(V1)),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3200,question,? [V1,V2] : ( $sum(f(f(V1)),1) = f(V1) & $greater(f(f(V1)),V2) & $int(V1) & $sum($sum(f(f(V1)),1),2) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 285.83 CPU 295.06 WC Sending question: fof(sum_equal_1_Q3205,question,? [V1] : ( $sum(f(V1),1) = V1 & $int(f(f(V1))) & $greater(f(V1),$sum(f(V1),2)) & $sum(f(V1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3227,question,? [V1] : ( $sum(f(V1),2) = f(V1) & $greater(f(f(V1)),$sum(f(V1),2)) & $int(V1) & $sum(f(f(V1)),1) = V1 ),unknown,[xdb(limit,number(3))]). WATCH: 288.83 CPU 298.07 WC Sending question: fof(sum_equal_1_Q3234,question,? [V1,V2] : ( $sum(f(f(V1)),1) = f(V1) & $int(V1) & $sum($sum(f(f(V1)),1),2) = f(V1) & $greater(V2,f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q3238,question,? [V1,V2] : ( $greater(f(V1),V2) & $int(V1) & $sum(f(f(V1)),1) = f(V1) & $sum($sum(f(f(V1)),1),2) = f(V1) ),unknown,[xdb(limit,number(3))]). WATCH: 291.82 CPU 301.08 WC Sending question: fof(sum_equal_1_Q3267,question,? [V1,V2,V3] : ( $sum(V1,2) = V2 & $sum(f(f(V2)),1) = f(V2) & $int(V3) & $greater(f(f(V3)),$sum(f(f(V2)),1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(greater_1_Q3280,question,? [V1,V2] : ( $greater(f(V1),f(V1)) & $sum(f(f(V1)),2) = f(V1) & V2 = $sum($sum(f(f(V1)),2),1) & $int(V1) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3289,question,? [V1,V2,V3] : ( $sum(f(f(V1)),2) = f(V1) & $sum(V2,1) = V1 & $int(V3) & $greater($sum(f(f(V1)),2),f(f(V3))) ),unknown,[xdb(limit,number(3))]). WATCH: 294.81 CPU 304.09 WC Sending question: fof(sum_equal_1_Q3296,question,? [V1] : ( $sum($sum(f(V1),2),1) = V1 & $sum(f(V1),2) = f(V1) & $int(f(f(V1))) & $greater(f(V1),f(V1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3306,question,? [V1,V2] : ( $sum(f(V1),1) = f(V1) & $int(V2) & $sum(f(V1),2) = V1 & $greater($sum(f(V1),1),f(f(f(V2)))) ),unknown,[xdb(limit,number(3))]). WATCH: 297.81 CPU 307.10 WC Sending question: fof(equal_sum_1_Q3307,question,? [V1,V2] : ( f(f(V1)) = $sum(V2,1) & f(V1) = $sum($sum(V2,1),2) & $int(V1) & $greater($sum(V2,1),$sum(V2,1)) ),unknown,[xdb(limit,number(3))]). Sending question: fof(sum_equal_1_Q3319,question,? [V1] : ( $sum(V1,2) = $sum(V1,1) & $int(V1) & f($sum(V1,2)) = $sum(V1,1) & $greater($sum(V1,1),$sum(V1,1)) ),unknown,[xdb(limit,number(3))]). WATCH: 300.80 CPU 310.11 WC FINAL WATCH: 300.80 CPU 310.21 WC