The cat eats the cow. The cat is rough. The cat likes the cow. The cat likes the rabbit. The cat likes the squirrel. The cow eats the squirrel. The cow is big. The cow needs the cat. The rabbit eats the squirrel. The rabbit needs the cow. The squirrel eats the cow. The squirrel is rough. If someone is big and cold then they eat the cat. All big people are cold. If someone needs the squirrel and the squirrel likes the cow then the squirrel needs the rabbit. All rough people are big. If someone needs the squirrel then they are rough. If someone needs the rabbit and they need the cat then they eat the cow. If someone likes the rabbit and they eat the cow then the cow eats the cat. If the squirrel is blue then the squirrel needs the cow.
The cat eats the cow.
("cat" "eats" "cow" "+")
The cat is rough.
("cat" "is" "rough" "+")
The cat likes the cow.
("cat" "likes" "cow" "+")
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is big.
("cow" "is" "big" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
If someone is big and cold then they eat the cat.
((("someone" "is" "big" "+") ("someone" "is" "cold" "+")) -> ("someone" "eats" "cat" "+"))
All big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone needs the squirrel and the squirrel likes the cow then the squirrel needs the rabbit.
((("someone" "needs" "squirrel" "+") ("squirrel" "likes" "cow" "+")) -> ("squirrel" "needs" "rabbit" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
If someone needs the squirrel then they are rough.
((("someone" "needs" "squirrel" "+")) -> ("someone" "is" "rough" "+"))
If someone needs the rabbit and they need the cat then they eat the cow.
((("someone" "needs" "rabbit" "+") ("someone" "needs" "cat" "+")) -> ("someone" "eats" "cow" "+"))
If someone likes the rabbit and they eat the cow then the cow eats the cat.
((("someone" "likes" "rabbit" "+") ("someone" "eats" "cow" "+")) -> ("cow" "eats" "cat" "+"))
If the squirrel is blue then the squirrel needs the cow.
((("squirrel" "is" "blue" "+")) -> ("squirrel" "needs" "cow" "+"))
The cow needs the cat.
True
1
proof
[(triple8)]
("cow" "needs" "cat" "+")
triple8
The cat does not like the squirrel.
False
1
inv-proof
[(triple5)]
("cat" "likes" "squirrel" "-")
triple5
The cat is big.
True
2
proof
[(((triple2) -> rule4))]
("cat" "is" "big" "+")
((triple2) -> (rule4 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple2) -> rule4))]
("cat" "is" "big" "-")
((triple2) -> (rule4 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The squirrel is cold.
True
3
proof
[(((((triple12) -> rule4)) -> rule2))]
("squirrel" "is" "cold" "+")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is not cold.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule2))]
("squirrel" "is" "cold" "-")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel eats the cat.
True
6
proof
[(((((triple12) -> rule4) ((((triple12) -> rule4)) -> rule2)) -> rule1))]
("squirrel" "eats" "cat" "+")
((((triple12) -> (rule4 % int3)) ((((triple12) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The cat does not eat the cat.
False
6
inv-proof
[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule1))]
("cat" "eats" "cat" "-")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The squirrel does not need the rabbit.
Unknown
inv-rconc
[@1: The squirrel needs the rabbit.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "needs" "rabbit" "-")
The cow is rough.
Unknown
rconc
[@1: The cow is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "rough" "+")
The rabbit does not eat the cow.
Unknown
inv-rconc
[@1: The rabbit eats the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("rabbit" "eats" "cow" "-")
The rabbit is rough.
Unknown
rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "rough" "+")
The cow does not need the rabbit.
Unknown
inv-random
[@0: The cow needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "rabbit" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
The squirrel is not red.
Unknown
inv-random
[@0: The squirrel is red.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "red" "-")
The rabbit likes the rabbit.
Unknown
random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "+")
@0: The cat eats the cow.[(triple1)] The cat is rough.[(triple2)] The cat likes the cow.[(triple3)] The cat likes the rabbit.[(triple4)] The cat likes the squirrel.[(triple5)] The cow eats the squirrel.[(triple6)] The cow is big.[(triple7)] The cow needs the cat.[(triple8)] The rabbit eats the squirrel.[(triple9)] The rabbit needs the cow.[(triple10)] The squirrel eats the cow.[(triple11)] The squirrel is rough.[(triple12)] @1: The cat is big.[(((triple2) -> rule4))] The cow eats the cat.[(((triple4 triple1) -> rule7) OR ((triple7 ((triple7) -> rule2)) -> rule1))] The cow is cold.[(((triple7) -> rule2))] The squirrel is big.[(((triple12) -> rule4))] @2: The cat is cold.[(((((triple2) -> rule4)) -> rule2))] The squirrel is cold.[(((((triple12) -> rule4)) -> rule2))] @3: The cat eats the cat.[(((((triple2) -> rule4) ((((triple2) -> rule4)) -> rule2)) -> rule1))] The squirrel eats the cat.[(((((triple12) -> rule4) ((((triple12) -> rule4)) -> rule2)) -> rule1))]
The cat eats the cow.
("cat" "eats" "cow" "+")
triple1
The cat is rough.
("cat" "is" "rough" "+")
triple2
The cat likes the cow.
("cat" "likes" "cow" "+")
triple3
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple4
The cat likes the squirrel.
("cat" "likes" "squirrel" "+")
triple5
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple6
The cow is big.
("cow" "is" "big" "+")
triple7
The cow needs the cat.
("cow" "needs" "cat" "+")
triple8
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple9
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple10
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple11
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple12
The cat is big.
("cat" "is" "big" "+")
((triple2) -> (rule4 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cow eats the cat.
("cow" "eats" "cat" "+")
((triple4 triple1) -> (rule7 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
((triple7 ((triple7) -> (rule2 % int2))) -> (rule1 % int1))
The cow eats the cat.
("cow" "eats" "cat" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
((triple7) -> (rule2 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
((triple12) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is big.
("cat" "is" "big" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The cat eats the cat.
("cat" "eats" "cat" "+")
((((triple2) -> (rule4 % int3)) ((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cat eats the cat.
("cat" "eats" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is big.
("cat" "is" "big" "+")
int3
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
((((triple12) -> (rule4 % int3)) ((((triple12) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3