The cat is blue. The cat is cold. The cat is red. The cat likes the lion. The cat needs the cow. The cat visits the lion. The cow is blue. The cow is young. The cow visits the lion. The lion is red. The lion likes the cat. The lion likes the cow. The lion needs the cat. The lion visits the cat. The lion visits the cow. If someone is young and they like the lion then the lion likes the cow. If someone needs the cat and they are cold then the cat is rough. If someone is red then they need the cow. If someone likes the cat and they are young then they need the lion. If the cat needs the cow and the cow is cold then the cow visits the lion. If someone is red and rough then they like the cat. If someone visits the cat then the cat likes the cow. If someone visits the lion and the lion needs the cow then they like the cat.
The cat is blue.
("cat" "is" "blue" "+")
The cat is cold.
("cat" "is" "cold" "+")
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat needs the cow.
("cat" "needs" "cow" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The cow is blue.
("cow" "is" "blue" "+")
The cow is young.
("cow" "is" "young" "+")
The cow visits the lion.
("cow" "visits" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The lion likes the cat.
("lion" "likes" "cat" "+")
The lion likes the cow.
("lion" "likes" "cow" "+")
The lion needs the cat.
("lion" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the cow.
("lion" "visits" "cow" "+")
If someone is young and they like the lion then the lion likes the cow.
((("someone" "is" "young" "+") ("someone" "likes" "lion" "+")) -> ("lion" "likes" "cow" "+"))
If someone needs the cat and they are cold then the cat is rough.
((("someone" "needs" "cat" "+") ("someone" "is" "cold" "+")) -> ("cat" "is" "rough" "+"))
If someone is red then they need the cow.
((("someone" "is" "red" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the cat and they are young then they need the lion.
((("someone" "likes" "cat" "+") ("someone" "is" "young" "+")) -> ("someone" "needs" "lion" "+"))
If the cat needs the cow and the cow is cold then the cow visits the lion.
((("cat" "needs" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "visits" "lion" "+"))
If someone is red and rough then they like the cat.
((("someone" "is" "red" "+") ("someone" "is" "rough" "+")) -> ("someone" "likes" "cat" "+"))
If someone visits the cat then the cat likes the cow.
((("someone" "visits" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If someone visits the lion and the lion needs the cow then they like the cat.
((("someone" "visits" "lion" "+") ("lion" "needs" "cow" "+")) -> ("someone" "likes" "cat" "+"))
The cat likes the lion.
True
1
proof
[(triple4)]
("cat" "likes" "lion" "+")
triple4
The cat is not red.
False
1
inv-proof
[(triple3)]
("cat" "is" "red" "-")
triple3
The cat likes the cow.
True
2
proof
[(((triple14) -> rule7))]
("cat" "likes" "cow" "+")
((triple14) -> (rule7 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion does not need the cow.
False
2
inv-proof
[(((triple10) -> rule3))]
("lion" "needs" "cow" "-")
((triple10) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cat likes the cat.
True
4
proof
[(((triple6 ((triple10) -> rule3)) -> rule8))]
("cat" "likes" "cat" "+")
((triple6 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The cow does not like the cat.
False
4
inv-proof
[(((triple9 ((triple10) -> rule3)) -> rule8))]
("cow" "likes" "cat" "-")
((triple9 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The cow needs the lion.
True
6
proof
[(((((triple9 ((triple10) -> rule3)) -> rule8) triple8) -> rule4))]
("cow" "needs" "lion" "+")
((((triple9 ((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple8) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3
The cow does not need the lion.
False
6
inv-proof
[(((((triple9 ((triple10) -> rule3)) -> rule8) triple8) -> rule4))]
("cow" "needs" "lion" "-")
((((triple9 ((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple8) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "needs" "cow" "-")
The cat needs the lion.
Unknown
rconc
[@1: The cat needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "needs" "lion" "+")
The lion does not need the lion.
Unknown
inv-rconc
[@1: The lion needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "needs" "lion" "-")
The cat is rough.
Unknown
rconc
[@1: The cat is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "rough" "+")
The cow does not visit the cat.
Unknown
inv-random
[@0: The cow visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cat" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
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 cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
@0: The cat is blue.[(triple1)] The cat is cold.[(triple2)] The cat is red.[(triple3)] The cat likes the lion.[(triple4)] The cat needs the cow.[(triple5 OR ((triple3) -> rule3))] The cat visits the lion.[(triple6)] The cow is blue.[(triple7)] The cow is young.[(triple8)] The cow visits the lion.[(triple9)] The lion is red.[(triple10)] The lion likes the cat.[(triple11)] The lion likes the cow.[(triple12)] The lion needs the cat.[(triple13)] The lion visits the cat.[(triple14)] The lion visits the cow.[(triple15)] @1: The cat likes the cow.[(((triple14) -> rule7))] The lion needs the cow.[(((triple10) -> rule3))] @2: The cat likes the cat.[(((triple6 ((triple10) -> rule3)) -> rule8))] The cow likes the cat.[(((triple9 ((triple10) -> rule3)) -> rule8))] @3: The cow needs the lion.[(((((triple9 ((triple10) -> rule3)) -> rule8) triple8) -> rule4))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat likes the lion.
("cat" "likes" "lion" "+")
triple4
The cat needs the cow.
("cat" "needs" "cow" "+")
triple5
((triple3) -> (rule3 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
triple6
The cow is blue.
("cow" "is" "blue" "+")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The cow visits the lion.
("cow" "visits" "lion" "+")
triple9
The lion is red.
("lion" "is" "red" "+")
triple10
The lion likes the cat.
("lion" "likes" "cat" "+")
triple11
The lion likes the cow.
("lion" "likes" "cow" "+")
triple12
The lion needs the cat.
("lion" "needs" "cat" "+")
triple13
The lion visits the cat.
("lion" "visits" "cat" "+")
triple14
The lion visits the cow.
("lion" "visits" "cow" "+")
triple15
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple14) -> (rule7 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
((triple10) -> (rule3 % int1))
The lion needs the cow.
("lion" "needs" "cow" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple6 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple9 ((triple10) -> (rule3 % int2))) -> (rule8 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The lion needs the cow.
("lion" "needs" "cow" "+")
int2
The cow needs the lion.
("cow" "needs" "lion" "+")
((((triple9 ((triple10) -> (rule3 % int3))) -> (rule8 % int2)) triple8) -> (rule4 % int1))
The cow needs the lion.
("cow" "needs" "lion" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The lion needs the cow.
("lion" "needs" "cow" "+")
int3