The bear eats the squirrel. The cow is cold. The squirrel is round. If someone chases the squirrel and they are cold then they are red. If someone visits the squirrel and the squirrel visits the bear then the bear is round. If the cow visits the squirrel then the cow eats the bear. If someone eats the bear then they eat the cow. If someone chases the cow and they visit the squirrel then they are round. If the squirrel is round then the squirrel eats the bear.
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
The cow is cold.
("cow" "is" "cold" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
If someone chases the squirrel and they are cold then they are red.
((("someone" "chases" "squirrel" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone visits the squirrel and the squirrel visits the bear then the bear is round.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "bear" "+")) -> ("bear" "is" "round" "+"))
If the cow visits the squirrel then the cow eats the bear.
((("cow" "visits" "squirrel" "+")) -> ("cow" "eats" "bear" "+"))
If someone eats the bear then they eat the cow.
((("someone" "eats" "bear" "+")) -> ("someone" "eats" "cow" "+"))
If someone chases the cow and they visit the squirrel then they are round.
((("someone" "chases" "cow" "+") ("someone" "visits" "squirrel" "+")) -> ("someone" "is" "round" "+"))
If the squirrel is round then the squirrel eats the bear.
((("squirrel" "is" "round" "+")) -> ("squirrel" "eats" "bear" "+"))
The cow is cold.
True
1
proof
[(triple2)]
("cow" "is" "cold" "+")
triple2
The squirrel is not round.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "round" "-")
triple3
The squirrel eats the bear.
True
2
proof
[(((triple3) -> rule6))]
("squirrel" "eats" "bear" "+")
((triple3) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel does not eat the bear.
False
2
inv-proof
[(((triple3) -> rule6))]
("squirrel" "eats" "bear" "-")
((triple3) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel eats the cow.
True
3
proof
[(((((triple3) -> rule6)) -> rule4))]
("squirrel" "eats" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The squirrel does not eat the cow.
False
3
inv-proof
[(((((triple3) -> rule6)) -> rule4))]
("squirrel" "eats" "cow" "-")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "round" "-")
The cow is red.
Unknown
rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "red" "+")
The cow does not eat the cow.
Unknown
inv-rconc
[@2: The cow eats the cow.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("cow" "eats" "cow" "-")
The squirrel is green.
Unknown
random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "+")
The bear does not visit the squirrel.
Unknown
inv-random
[@0: The bear visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "squirrel" "-")
The squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The bear eats the squirrel.[(triple1)] The cow is cold.[(triple2)] The squirrel is round.[(triple3)] @1: The squirrel eats the bear.[(((triple3) -> rule6))] @2: The squirrel eats the cow.[(((((triple3) -> rule6)) -> rule4))]
The bear eats the squirrel.
("bear" "eats" "squirrel" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The squirrel is round.
("squirrel" "is" "round" "+")
triple3
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
((triple3) -> (rule6 % int1))
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
int1
The squirrel eats the bear.
("squirrel" "eats" "bear" "+")
int2