The cow eats the dog. The cow is big. The cow is green. The cow needs the squirrel. The dog is cold. The dog is not red. The dog needs the cow. The dog does not see the squirrel. The squirrel is big. The squirrel is blue. If something needs the squirrel and it is big then the squirrel needs the cow. If something is cold and blue then it sees the squirrel. All green things are not red.
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is big.
("cow" "is" "big" "+")
The cow is green.
("cow" "is" "green" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog is not red.
("dog" "is" "red" "-")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
If something needs the squirrel and it is big then the squirrel needs the cow.
((("something" "needs" "squirrel" "+") ("something" "is" "big" "+")) -> ("squirrel" "needs" "cow" "+"))
If something is cold and blue then it sees the squirrel.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "sees" "squirrel" "+"))
All green things are not red.
((("something" "is" "green" "+")) -> ("something" "is" "red" "-"))
The squirrel is big.
True
1
proof
[(triple9)]
("squirrel" "is" "big" "+")
triple9
The dog sees the squirrel.
False
1
inv-proof
[(triple8)]
("dog" "sees" "squirrel" "+")
triple8
The squirrel needs the cow.
True
3
proof
[(((triple4 triple2) -> rule1))]
("squirrel" "needs" "cow" "+")
((triple4 triple2) -> (rule1 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1
The cow is red.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "is" "red" "+")
((triple3) -> (rule3 % int1))
The cow is not red.
("cow" "is" "red" "-")
int1
The cow does not see the squirrel.
Unknown
inv-rconc
[@1: The cow sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "sees" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The dog is not green.
Unknown
inv-random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
@0: The cow eats the dog.[(triple1)] The cow is big.[(triple2)] The cow is green.[(triple3)] The cow needs the squirrel.[(triple4)] The dog does not see the squirrel.[(triple8)] The dog is cold.[(triple5)] The dog is not red.[(triple6)] The dog needs the cow.[(triple7)] The squirrel is big.[(triple9)] The squirrel is blue.[(triple10)] @1: The cow is not red.[(((triple3) -> rule3))] The squirrel needs the cow.[(((triple4 triple2) -> rule1))]
The cow eats the dog.
("cow" "eats" "dog" "+")
triple1
The cow is big.
("cow" "is" "big" "+")
triple2
The cow is green.
("cow" "is" "green" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The dog does not see the squirrel.
("dog" "sees" "squirrel" "-")
triple8
The dog is cold.
("dog" "is" "cold" "+")
triple5
The dog is not red.
("dog" "is" "red" "-")
triple6
The dog needs the cow.
("dog" "needs" "cow" "+")
triple7
The squirrel is big.
("squirrel" "is" "big" "+")
triple9
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple10
The cow is not red.
("cow" "is" "red" "-")
((triple3) -> (rule3 % int1))
The cow is not red.
("cow" "is" "red" "-")
int1
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
((triple4 triple2) -> (rule1 % int1))
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
int1