The cat is blue. The cat likes the rabbit. The cat visits the cow. The cow is red. The cow likes the cat. The cow visits the cat. The rabbit is green. The rabbit likes the cow. The rabbit sees the cat. The rabbit sees the cow. The rabbit visits the cat. The rabbit visits the cow. If someone likes the cow then they are blue. If someone likes the cat then they are green. If someone is blue and they visit the cat then the cat visits the rabbit. If someone visits the rabbit then they are green. If the cow visits the cat and the cow visits the rabbit then the cow likes the rabbit. If the cow sees the cat and the cat sees the rabbit then the cow is blue.
The cat is blue.
("cat" "is" "blue" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow is red.
("cow" "is" "red" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow visits the cat.
("cow" "visits" "cat" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If someone likes the cow then they are blue.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "blue" "+"))
If someone likes the cat then they are green.
((("someone" "likes" "cat" "+")) -> ("someone" "is" "green" "+"))
If someone is blue and they visit the cat then the cat visits the rabbit.
((("someone" "is" "blue" "+") ("someone" "visits" "cat" "+")) -> ("cat" "visits" "rabbit" "+"))
If someone visits the rabbit then they are green.
((("someone" "visits" "rabbit" "+")) -> ("someone" "is" "green" "+"))
If the cow visits the cat and the cow visits the rabbit then the cow likes the rabbit.
((("cow" "visits" "cat" "+") ("cow" "visits" "rabbit" "+")) -> ("cow" "likes" "rabbit" "+"))
If the cow sees the cat and the cat sees the rabbit then the cow is blue.
((("cow" "sees" "cat" "+") ("cat" "sees" "rabbit" "+")) -> ("cow" "is" "blue" "+"))
The rabbit likes the cow.
True
1
proof
[(triple8)]
("rabbit" "likes" "cow" "+")
triple8
The cat does not visit the cow.
False
1
inv-proof
[(triple3)]
("cat" "visits" "cow" "-")
triple3
The cow is green.
True
2
proof
[(((triple5) -> rule2))]
("cow" "is" "green" "+")
((triple5) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple5) -> rule2))]
("cow" "is" "green" "-")
((triple5) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cat visits the rabbit.
True
4
proof
[(((((triple8) -> rule1) triple11) -> rule3))]
("cat" "visits" "rabbit" "+")
((((triple8) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat does not visit the rabbit.
False
4
inv-proof
[(((((triple8) -> rule1) triple11) -> rule3))]
("cat" "visits" "rabbit" "-")
((((triple8) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat is green.
True
5
proof
[(((((((triple8) -> rule1) triple11) -> rule3)) -> rule4))]
("cat" "is" "green" "+")
((((((triple8) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cat is not green.
False
5
inv-proof
[(((((((triple8) -> rule1) triple11) -> rule3)) -> rule4))]
("cat" "is" "green" "-")
((((((triple8) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3
The cow does not like the rabbit.
Unknown
inv-rconc
[@1: The cow likes the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "likes" "rabbit" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "blue" "+")
The cow does not see the rabbit.
Unknown
inv-random
[@0: The cow sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "rabbit" "-")
The cow visits the rabbit.
Unknown
random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "rabbit" "+")
The cat does not see the cow.
Unknown
inv-random
[@0: The cat sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cow" "-")
The cat sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat likes the cow.
Unknown
random
[@0: The cat likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cow" "+")
@0: The cat is blue.[(triple1)] The cat likes the rabbit.[(triple2)] The cat visits the cow.[(triple3)] The cow is red.[(triple4)] The cow likes the cat.[(triple5)] The cow visits the cat.[(triple6)] The rabbit is green.[(triple7)] The rabbit likes the cow.[(triple8)] The rabbit sees the cat.[(triple9)] The rabbit sees the cow.[(triple10)] The rabbit visits the cat.[(triple11)] The rabbit visits the cow.[(triple12)] @1: The cow is green.[(((triple5) -> rule2))] The rabbit is blue.[(((triple8) -> rule1))] @2: The cat visits the rabbit.[(((((triple8) -> rule1) triple11) -> rule3))] @3: The cat is green.[(((((((triple8) -> rule1) triple11) -> rule3)) -> rule4))]
The cat is blue.
("cat" "is" "blue" "+")
triple1
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple2
The cat visits the cow.
("cat" "visits" "cow" "+")
triple3
The cow is red.
("cow" "is" "red" "+")
triple4
The cow likes the cat.
("cow" "likes" "cat" "+")
triple5
The cow visits the cat.
("cow" "visits" "cat" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple7
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple8
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple9
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple10
The rabbit visits the cat.
("rabbit" "visits" "cat" "+")
triple11
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple12
The cow is green.
("cow" "is" "green" "+")
((triple5) -> (rule2 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
((triple8) -> (rule1 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((((triple8) -> (rule1 % int2)) triple11) -> (rule3 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The cat is green.
("cat" "is" "green" "+")
((((((triple8) -> (rule1 % int3)) triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit is blue.
("rabbit" "is" "blue" "+")
int3