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