The cow eats the lion. The cow is not green. The cow likes the squirrel. The cow needs the squirrel. The lion eats the squirrel. The lion is not round. The lion needs the cow. The squirrel eats the lion. The squirrel likes the lion. The squirrel needs the cow. If someone likes the cow then the cow eats the squirrel. If the squirrel likes the cow and the squirrel needs the cow then the squirrel eats the lion. If the cow does not like the squirrel then the squirrel does not need the cow. If the squirrel eats the lion and the lion likes the squirrel then the squirrel needs the cow. If someone likes the lion then they do not eat the squirrel. If someone needs the squirrel then they need the cow. If someone likes the squirrel then they like the cow. If the lion does not like the cow then the cow is red.
The cow eats the lion.
("cow" "eats" "lion" "+")
The cow is not green.
("cow" "is" "green" "-")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
The lion is not round.
("lion" "is" "round" "-")
The lion needs the cow.
("lion" "needs" "cow" "+")
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If someone likes the cow then the cow eats the squirrel.
((("someone" "likes" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If the squirrel likes the cow and the squirrel needs the cow then the squirrel eats the lion.
((("squirrel" "likes" "cow" "+") ("squirrel" "needs" "cow" "+")) -> ("squirrel" "eats" "lion" "+"))
If the cow does not like the squirrel then the squirrel does not need the cow.
((("cow" "likes" "squirrel" "~")) -> ("squirrel" "needs" "cow" "-"))
If the squirrel eats the lion and the lion likes the squirrel then the squirrel needs the cow.
((("squirrel" "eats" "lion" "+") ("lion" "likes" "squirrel" "+")) -> ("squirrel" "needs" "cow" "+"))
If someone likes the lion then they do not eat the squirrel.
((("someone" "likes" "lion" "+")) -> ("someone" "eats" "squirrel" "-"))
If someone needs the squirrel then they need the cow.
((("someone" "needs" "squirrel" "+")) -> ("someone" "needs" "cow" "+"))
If someone likes the squirrel then they like the cow.
((("someone" "likes" "squirrel" "+")) -> ("someone" "likes" "cow" "+"))
If the lion does not like the cow then the cow is red.
((("lion" "likes" "cow" "~")) -> ("cow" "is" "red" "+"))
The squirrel likes the lion.
True
1
proof
[(triple9)]
("squirrel" "likes" "lion" "+")
triple9
The squirrel does not need the cow.
False
1
inv-proof
[(triple10)]
("squirrel" "needs" "cow" "-")
triple10
The cow needs the cow.
True
2
proof
[(((triple4) -> rule6))]
("cow" "needs" "cow" "+")
((triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple3) -> rule7))]
("cow" "likes" "cow" "-")
((triple3) -> (rule7 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow eats the squirrel.
True
3
proof
[(((((triple3) -> rule7)) -> rule1))]
("cow" "eats" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not eat the squirrel.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule1))]
("cow" "eats" "squirrel" "-")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The squirrel does not like the cow.
Unknown
inv-rconc
[@1: The squirrel likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "likes" "cow" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "likes" "cow" "+")
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "is" "red" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The lion needs the lion.
Unknown
random
[@0: The lion needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "lion" "+")
@0: The cow eats the lion.[(triple1)] The cow is not green.[(triple2)] The cow likes the squirrel.[(triple3)] The cow needs the squirrel.[(triple4)] The lion eats the squirrel.[(triple5)] The lion is not round.[(triple6)] The lion needs the cow.[(triple7)] The squirrel eats the lion.[(triple8)] The squirrel likes the lion.[(triple9)] The squirrel needs the cow.[(triple10)] @1: The cow likes the cow.[(((triple3) -> rule7))] The cow needs the cow.[(((triple4) -> rule6))] The squirrel does not eat the squirrel.[(((triple9) -> rule5))] @2: The cow eats the squirrel.[(((((triple3) -> rule7)) -> rule1))]
The cow eats the lion.
("cow" "eats" "lion" "+")
triple1
The cow is not green.
("cow" "is" "green" "-")
triple2
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The lion eats the squirrel.
("lion" "eats" "squirrel" "+")
triple5
The lion is not round.
("lion" "is" "round" "-")
triple6
The lion needs the cow.
("lion" "needs" "cow" "+")
triple7
The squirrel eats the lion.
("squirrel" "eats" "lion" "+")
triple8
The squirrel likes the lion.
("squirrel" "likes" "lion" "+")
triple9
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple10
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple3) -> (rule7 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow needs the cow.
("cow" "needs" "cow" "+")
((triple4) -> (rule6 % int1))
The cow needs the cow.
("cow" "needs" "cow" "+")
int1
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
((triple9) -> (rule5 % int1))
The squirrel does not eat the squirrel.
("squirrel" "eats" "squirrel" "-")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((((triple3) -> (rule7 % int2))) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2