The cow eats the squirrel. The squirrel eats the cow. The squirrel needs the cow. If someone needs the cow then the cow chases the squirrel. If someone chases the squirrel and the squirrel needs the cow then they chase the cow.
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
If someone needs the cow then the cow chases the squirrel.
((("someone" "needs" "cow" "+")) -> ("cow" "chases" "squirrel" "+"))
If someone chases the squirrel and the squirrel needs the cow then they chase the cow.
((("someone" "chases" "squirrel" "+") ("squirrel" "needs" "cow" "+")) -> ("someone" "chases" "cow" "+"))
The cow eats the squirrel.
True
1
proof
[(triple1)]
("cow" "eats" "squirrel" "+")
triple1
The squirrel does not eat the cow.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "cow" "-")
triple2
The cow chases the squirrel.
True
2
proof
[(((triple3) -> rule1))]
("cow" "chases" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow does not chase the squirrel.
False
2
inv-proof
[(((triple3) -> rule1))]
("cow" "chases" "squirrel" "-")
((triple3) -> (rule1 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow chases the cow.
True
4
proof
[(((((triple3) -> rule1) triple3) -> rule2))]
("cow" "chases" "cow" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The cow does not chase the cow.
False
4
inv-proof
[(((((triple3) -> rule1) triple3) -> rule2))]
("cow" "chases" "cow" "-")
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2
The squirrel does not chase the cow.
Unknown
inv-rconc
[@1: The squirrel chases the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "chases" "cow" "-")
The cow is rough.
Unknown
random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The cow is red.
Unknown
random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "+")
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 squirrel eats the squirrel.
Unknown
random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "+")
@0: The cow eats the squirrel.[(triple1)] The squirrel eats the cow.[(triple2)] The squirrel needs the cow.[(triple3)] @1: The cow chases the squirrel.[(((triple3) -> rule1))] @2: The cow chases the cow.[(((((triple3) -> rule1) triple3) -> rule2))]
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple1
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple2
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple3
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
((triple3) -> (rule1 % int1))
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
((((triple3) -> (rule1 % int2)) triple3) -> (rule2 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
int2