The cat eats the rabbit. The cat eats the squirrel. The cat is big. The cat is green. The cat visits the lion. The lion eats the rabbit. The lion is blue. The lion is young. The lion visits the cat. The rabbit eats the squirrel. The rabbit is young. The rabbit does not visit the cat. The squirrel eats the rabbit. The squirrel is green. The squirrel needs the lion. The squirrel visits the lion. If something eats the cat and the cat visits the rabbit then it is not rough. If something visits the cat and the cat is not young then it is big. If something needs the rabbit then it eats the cat. If something is rough then it eats the cat. If something eats the squirrel then it needs the rabbit. If something eats the squirrel then it visits the rabbit. If something visits the squirrel and the squirrel does not need the rabbit then the squirrel eats the rabbit. If something visits the squirrel and it does not visit the rabbit then the rabbit visits the lion.
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is green.
("cat" "is" "green" "+")
The cat visits the lion.
("cat" "visits" "lion" "+")
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is young.
("lion" "is" "young" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
If something eats the cat and the cat visits the rabbit then it is not rough.
((("something" "eats" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("something" "is" "rough" "-"))
If something visits the cat and the cat is not young then it is big.
((("something" "visits" "cat" "+") ("cat" "is" "young" "~")) -> ("something" "is" "big" "+"))
If something needs the rabbit then it eats the cat.
((("something" "needs" "rabbit" "+")) -> ("something" "eats" "cat" "+"))
If something is rough then it eats the cat.
((("something" "is" "rough" "+")) -> ("something" "eats" "cat" "+"))
If something eats the squirrel then it needs the rabbit.
((("something" "eats" "squirrel" "+")) -> ("something" "needs" "rabbit" "+"))
If something eats the squirrel then it visits the rabbit.
((("something" "eats" "squirrel" "+")) -> ("something" "visits" "rabbit" "+"))
If something visits the squirrel and the squirrel does not need the rabbit then the squirrel eats the rabbit.
((("something" "visits" "squirrel" "+") ("squirrel" "needs" "rabbit" "~")) -> ("squirrel" "eats" "rabbit" "+"))
If something visits the squirrel and it does not visit the rabbit then the rabbit visits the lion.
((("something" "visits" "squirrel" "+") ("something" "visits" "rabbit" "~")) -> ("rabbit" "visits" "lion" "+"))
The rabbit eats the squirrel.
True
1
proof
[(triple10)]
("rabbit" "eats" "squirrel" "+")
triple10
The cat does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("cat" "eats" "squirrel" "-")
triple2
The rabbit visits the rabbit.
True
2
proof
[(((triple10) -> rule6))]
("rabbit" "visits" "rabbit" "+")
((triple10) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not need the rabbit.
False
2
inv-proof
[(((triple10) -> rule5))]
("rabbit" "needs" "rabbit" "-")
((triple10) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The cat eats the cat.
True
3
proof
[(((((triple2) -> rule5)) -> rule3))]
("cat" "eats" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The rabbit does not eat the cat.
False
3
inv-proof
[(((((triple10) -> rule5)) -> rule3))]
("rabbit" "eats" "cat" "-")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The cat is not rough.
True
6
proof
[(((((((triple2) -> rule5)) -> rule3) ((triple2) -> rule6)) -> rule1))]
("cat" "is" "rough" "-")
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int4
The rabbit is rough.
False
6
inv-proof
[(((((((triple10) -> rule5)) -> rule3) ((triple2) -> rule6)) -> rule1))]
("rabbit" "is" "rough" "+")
((((((triple10) -> (rule5 % int4))) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The lion does not visit the rabbit.
Unknown
inv-rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "visits" "rabbit" "-")
The squirrel needs the rabbit.
Unknown
rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("squirrel" "needs" "rabbit" "+")
The squirrel does not eat the cat.
Unknown
inv-rconc
[@2: The squirrel eats the cat.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("squirrel" "eats" "cat" "-")
The rabbit visits the lion.
Unknown
rconc
[@1: The rabbit visits the lion.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "visits" "lion" "+")
The squirrel does not visit the cat.
Unknown
inv-random
[@0: The squirrel visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cat" "-")
The lion eats the lion.
Unknown
random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "+")
The cat is not blue.
Unknown
inv-random
[@0: The cat is blue.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "blue" "-")
The rabbit needs the squirrel.
Unknown
random
[@0: The rabbit needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "squirrel" "+")
@0: The cat eats the rabbit.[(triple1)] The cat eats the squirrel.[(triple2)] The cat is big.[(triple3)] The cat is green.[(triple4)] The cat visits the lion.[(triple5)] The lion eats the rabbit.[(triple6)] The lion is blue.[(triple7)] The lion is young.[(triple8)] The lion visits the cat.[(triple9)] The rabbit does not visit the cat.[(triple12)] The rabbit eats the squirrel.[(triple10)] The rabbit is young.[(triple11)] The squirrel eats the rabbit.[(triple13)] The squirrel is green.[(triple14)] The squirrel needs the lion.[(triple15)] The squirrel visits the lion.[(triple16)] @1: The cat needs the rabbit.[(((triple2) -> rule5))] The cat visits the rabbit.[(((triple2) -> rule6))] The rabbit needs the rabbit.[(((triple10) -> rule5))] The rabbit visits the rabbit.[(((triple10) -> rule6))] @2: The cat eats the cat.[(((((triple2) -> rule5)) -> rule3))] The rabbit eats the cat.[(((((triple10) -> rule5)) -> rule3))] @3: The cat is not rough.[(((((((triple2) -> rule5)) -> rule3) ((triple2) -> rule6)) -> rule1))] The rabbit is not rough.[(((((((triple10) -> rule5)) -> rule3) ((triple2) -> rule6)) -> rule1))]
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple1
The cat eats the squirrel.
("cat" "eats" "squirrel" "+")
triple2
The cat is big.
("cat" "is" "big" "+")
triple3
The cat is green.
("cat" "is" "green" "+")
triple4
The cat visits the lion.
("cat" "visits" "lion" "+")
triple5
The lion eats the rabbit.
("lion" "eats" "rabbit" "+")
triple6
The lion is blue.
("lion" "is" "blue" "+")
triple7
The lion is young.
("lion" "is" "young" "+")
triple8
The lion visits the cat.
("lion" "visits" "cat" "+")
triple9
The rabbit does not visit the cat.
("rabbit" "visits" "cat" "-")
triple12
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple10
The rabbit is young.
("rabbit" "is" "young" "+")
triple11
The squirrel eats the rabbit.
("squirrel" "eats" "rabbit" "+")
triple13
The squirrel is green.
("squirrel" "is" "green" "+")
triple14
The squirrel needs the lion.
("squirrel" "needs" "lion" "+")
triple15
The squirrel visits the lion.
("squirrel" "visits" "lion" "+")
triple16
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
((triple2) -> (rule5 % int1))
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
((triple2) -> (rule6 % int1))
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((triple10) -> (rule5 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple10) -> (rule6 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The cat is not rough.
("cat" "is" "rough" "-")
((((((triple2) -> (rule5 % int4))) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The cat is not rough.
("cat" "is" "rough" "-")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
int3
The cat needs the rabbit.
("cat" "needs" "rabbit" "+")
int4
The rabbit is not rough.
("rabbit" "is" "rough" "-")
((((((triple10) -> (rule5 % int4))) -> (rule3 % int3)) ((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is not rough.
("rabbit" "is" "rough" "-")
int1
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
int2
The rabbit eats the cat.
("rabbit" "eats" "cat" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4