The cat eats the lion. The cat is big. The cat is blue. The cat is cold. The cat is red. The cat is rough. The cat needs the lion. The cat visits the lion. The lion eats the cat. The lion is big. The lion is blue. The lion is cold. The lion is red. The lion needs the cat. The lion visits the cat. If someone is cold and they visit the cat then they eat the cat. If someone eats the lion and the lion eats the cat then they visit the cat. If someone visits the lion and they visit the cat then the cat is big. If the cat visits the lion then the cat needs the lion. If someone needs the lion then the lion visits the cat. If someone needs the cat then they eat the cat.
The cat eats the lion.
("cat" "eats" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion is big.
("lion" "is" "big" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is cold.
("lion" "is" "cold" "+")
The lion is red.
("lion" "is" "red" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone is cold and they visit the cat then they eat the cat.
((("someone" "is" "cold" "+") ("someone" "visits" "cat" "+")) -> ("someone" "eats" "cat" "+"))
If someone eats the lion and the lion eats the cat then they visit the cat.
((("someone" "eats" "lion" "+") ("lion" "eats" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone visits the lion and they visit the cat then the cat is big.
((("someone" "visits" "lion" "+") ("someone" "visits" "cat" "+")) -> ("cat" "is" "big" "+"))
If the cat visits the lion then the cat needs the lion.
((("cat" "visits" "lion" "+")) -> ("cat" "needs" "lion" "+"))
If someone needs the lion then the lion visits the cat.
((("someone" "needs" "lion" "+")) -> ("lion" "visits" "cat" "+"))
If someone needs the cat then they eat the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "eats" "cat" "+"))
The cat is big.
True
1
proof
[(triple2 OR ((triple8 ((triple1 triple9) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple14) -> rule6)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 triple15) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "big" "+")
triple2
((triple8 ((triple1 triple9) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((triple8 ((triple1 ((triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 ((triple7) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
((triple8 ((triple1 ((triple12 ((((triple8) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
The cat is not big.
False
1
inv-proof
[(triple2 OR ((triple8 ((triple1 triple9) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple14) -> rule6)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 triple15) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2)) -> rule3))]
("cat" "is" "big" "-")
triple2
((triple8 ((triple1 triple9) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((triple8 ((triple1 ((triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 ((triple7) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
((triple8 ((triple1 ((triple12 ((((triple8) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
The cat visits the cat.
True
3
proof
[(((triple1 triple9) -> rule2) OR ((triple1 ((triple14) -> rule6)) -> rule2) OR ((triple1 ((triple12 triple15) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2))]
("cat" "visits" "cat" "+")
((triple1 triple9) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((triple1 ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 ((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple1 ((triple12 ((((triple8) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The cat does not visit the cat.
False
3
inv-proof
[(((triple1 triple9) -> rule2) OR ((triple1 ((triple14) -> rule6)) -> rule2) OR ((triple1 ((triple12 triple15) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2))]
("cat" "visits" "cat" "-")
((triple1 triple9) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((triple1 ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 ((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple1 ((triple12 ((((triple8) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The lion does not need the lion.
Unknown
inv-random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
@0: The cat eats the lion.[(triple1)] The cat is big.[(triple2 OR ((triple8 ((triple1 triple9) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple14) -> rule6)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 triple15) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2)) -> rule3) OR ((triple8 ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2)) -> rule3))] The cat is blue.[(triple3)] The cat is cold.[(triple4)] The cat is red.[(triple5)] The cat is rough.[(triple6)] The cat needs the lion.[(triple7 OR ((triple8) -> rule4))] The cat visits the lion.[(triple8)] The lion eats the cat.[(triple9 OR ((triple14) -> rule6) OR ((triple12 triple15) -> rule1) OR ((triple12 ((triple7) -> rule5)) -> rule1) OR ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1))] The lion is big.[(triple10)] The lion is blue.[(triple11)] The lion is cold.[(triple12)] The lion is red.[(triple13)] The lion needs the cat.[(triple14)] The lion visits the cat.[(triple15 OR ((triple7) -> rule5) OR ((((triple8) -> rule4)) -> rule5))] @1: The cat visits the cat.[(((triple1 triple9) -> rule2) OR ((triple1 ((triple14) -> rule6)) -> rule2) OR ((triple1 ((triple12 triple15) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2) OR ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2))] @2: The cat eats the cat.[(((triple4 ((triple1 triple9) -> rule2)) -> rule1) OR ((triple4 ((triple1 ((triple14) -> rule6)) -> rule2)) -> rule1) OR ((triple4 ((triple1 ((triple12 triple15) -> rule1)) -> rule2)) -> rule1) OR ((triple4 ((triple1 ((triple12 ((triple7) -> rule5)) -> rule1)) -> rule2)) -> rule1) OR ((triple4 ((triple1 ((triple12 ((((triple8) -> rule4)) -> rule5)) -> rule1)) -> rule2)) -> rule1))]
The cat eats the lion.
("cat" "eats" "lion" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
((triple8 ((triple1 triple9) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((triple8 ((triple1 ((triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple8 ((triple1 ((triple12 ((triple7) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
((triple8 ((triple1 ((triple12 ((((triple8) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5
The cat is blue.
("cat" "is" "blue" "+")
triple3
The cat is cold.
("cat" "is" "cold" "+")
triple4
The cat is red.
("cat" "is" "red" "+")
triple5
The cat is rough.
("cat" "is" "rough" "+")
triple6
The cat needs the lion.
("cat" "needs" "lion" "+")
triple7
((triple8) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple8
The lion eats the cat.
("lion" "eats" "cat" "+")
triple9
((triple14) -> (rule6 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
((triple12 triple15) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
((triple12 ((triple7) -> (rule5 % int2))) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
((triple12 ((((triple8) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The lion eats the cat.
("lion" "eats" "cat" "+")
int1
The lion visits the cat.
("lion" "visits" "cat" "+")
int2
The cat needs the lion.
("cat" "needs" "lion" "+")
int3
The lion is big.
("lion" "is" "big" "+")
triple10
The lion is blue.
("lion" "is" "blue" "+")
triple11
The lion is cold.
("lion" "is" "cold" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
triple13
The lion needs the cat.
("lion" "needs" "cat" "+")
triple14
The lion visits the cat.
("lion" "visits" "cat" "+")
triple15
((triple7) -> (rule5 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
The lion visits the cat.
("lion" "visits" "cat" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
int2
The cat visits the cat.
("cat" "visits" "cat" "+")
((triple1 triple9) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
((triple1 ((triple14) -> (rule6 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 triple15) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
((triple1 ((triple12 ((triple7) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
((triple1 ((triple12 ((((triple8) -> (rule4 % int4))) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The lion eats the cat.
("lion" "eats" "cat" "+")
int2
The lion visits the cat.
("lion" "visits" "cat" "+")
int3
The cat needs the lion.
("cat" "needs" "lion" "+")
int4
The cat eats the cat.
("cat" "eats" "cat" "+")
((triple4 ((triple1 triple9) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
((triple4 ((triple1 ((triple14) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple4 ((triple1 ((triple12 triple15) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
((triple4 ((triple1 ((triple12 ((triple7) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
((triple4 ((triple1 ((triple12 ((((triple8) -> (rule4 % int5))) -> (rule5 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The lion eats the cat.
("lion" "eats" "cat" "+")
int3
The lion visits the cat.
("lion" "visits" "cat" "+")
int4
The cat needs the lion.
("cat" "needs" "lion" "+")
int5