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