The bear needs the cow. The cow needs the bear. The squirrel eats the cow. If the bear needs the cow then the cow eats the squirrel. If something eats the squirrel and the squirrel eats the cow then the cow is kind.
The bear needs the cow.
("bear" "needs" "cow" "+")
The cow needs the bear.
("cow" "needs" "bear" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
If the bear needs the cow then the cow eats the squirrel.
((("bear" "needs" "cow" "+")) -> ("cow" "eats" "squirrel" "+"))
If something eats the squirrel and the squirrel eats the cow then the cow is kind.
((("something" "eats" "squirrel" "+") ("squirrel" "eats" "cow" "+")) -> ("cow" "is" "kind" "+"))
The cow needs the bear.
True
1
proof
[(triple2)]
("cow" "needs" "bear" "+")
triple2
The bear does not need the cow.
False
1
inv-proof
[(triple1)]
("bear" "needs" "cow" "-")
triple1
The cow eats the squirrel.
True
2
proof
[(((triple1) -> rule1))]
("cow" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow does not eat the squirrel.
False
2
inv-proof
[(((triple1) -> rule1))]
("cow" "eats" "squirrel" "-")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is kind.
True
4
proof
[(((((triple1) -> rule1) triple3) -> rule2))]
("cow" "is" "kind" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow is not kind.
False
4
inv-proof
[(((((triple1) -> rule1) triple3) -> rule2))]
("cow" "is" "kind" "-")
((((triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2
The cow does not eat the cow.
Unknown
inv-random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "-")
The cow eats the bear.
Unknown
random
[@0: The cow eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "bear" "+")
The squirrel does not see the bear.
Unknown
inv-random
[@0: The squirrel sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "bear" "-")
The bear is kind.
Unknown
random
[@0: The bear is kind.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "kind" "+")
The cow does not need the squirrel.
Unknown
inv-random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "-")
The bear eats the squirrel.
Unknown
random
[@0: The bear eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "squirrel" "+")
@0: The bear needs the cow.[(triple1)] The cow needs the bear.[(triple2)] The squirrel eats the cow.[(triple3)] @1: The cow eats the squirrel.[(((triple1) -> rule1))] @2: The cow is kind.[(((((triple1) -> rule1) triple3) -> rule2))]
The bear needs the cow.
("bear" "needs" "cow" "+")
triple1
The cow needs the bear.
("cow" "needs" "bear" "+")
triple2
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple3
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
((triple1) -> (rule1 % int1))
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int1
The cow is kind.
("cow" "is" "kind" "+")
((((triple1) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow is kind.
("cow" "is" "kind" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
int2