The bald eagle is not green. The bald eagle is red. The cat is red. The cat needs the squirrel. The cow eats the squirrel. The cow is green. The cow is not rough. The cow is young. The cow needs the cat. The cow needs the squirrel. The cow sees the cat. The squirrel eats the cat. The squirrel is red. The squirrel needs the cat. The squirrel sees the bald eagle. The squirrel sees the cat. If something sees the squirrel and it eats the cat then the squirrel needs the cat. If something needs the cat and it is not cold then the cat does not see the squirrel. If something eats the cat then it is red. If something needs the cat then it needs the squirrel. If something sees the cat then the cat needs the squirrel. If something is rough then it does not see the cat.
The bald eagle is not green.
("bald eagle" "is" "green" "-")
The bald eagle is red.
("bald eagle" "is" "red" "+")
The cat is red.
("cat" "is" "red" "+")
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is not rough.
("cow" "is" "rough" "-")
The cow is young.
("cow" "is" "young" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The cow sees the cat.
("cow" "sees" "cat" "+")
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
If something sees the squirrel and it eats the cat then the squirrel needs the cat.
((("something" "sees" "squirrel" "+") ("something" "eats" "cat" "+")) -> ("squirrel" "needs" "cat" "+"))
If something needs the cat and it is not cold then the cat does not see the squirrel.
((("something" "needs" "cat" "+") ("something" "is" "cold" "~")) -> ("cat" "sees" "squirrel" "-"))
If something eats the cat then it is red.
((("something" "eats" "cat" "+")) -> ("something" "is" "red" "+"))
If something needs the cat then it needs the squirrel.
((("something" "needs" "cat" "+")) -> ("something" "needs" "squirrel" "+"))
If something sees the cat then the cat needs the squirrel.
((("something" "sees" "cat" "+")) -> ("cat" "needs" "squirrel" "+"))
If something is rough then it does not see the cat.
((("something" "is" "rough" "+")) -> ("something" "sees" "cat" "-"))
The cow needs the squirrel.
True
1
proof
[(triple10 OR ((triple9) -> rule4))]
("cow" "needs" "squirrel" "+")
triple10
((triple9) -> (rule4 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow does not see the cat.
False
1
inv-proof
[(triple11)]
("cow" "sees" "cat" "-")
triple11
The squirrel needs the squirrel.
True
2
proof
[(((triple14) -> rule4))]
("squirrel" "needs" "squirrel" "+")
((triple14) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The squirrel does not need the squirrel.
False
2
inv-proof
[(((triple14) -> rule4))]
("squirrel" "needs" "squirrel" "-")
((triple14) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1
The cow is not red.
Unknown
inv-rconc
[@1: The cow is red.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cow" "is" "red" "-")
The bald eagle needs the squirrel.
Unknown
rconc
[@1: The bald eagle needs the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("bald eagle" "needs" "squirrel" "+")
The squirrel does not eat the cow.
Unknown
inv-random
[@0: The squirrel eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "cow" "-")
The squirrel needs the bald eagle.
Unknown
random
[@0: The squirrel needs the bald eagle.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "bald eagle" "+")
@0: The bald eagle is not green.[(triple1)] The bald eagle is red.[(triple2)] The cat is red.[(triple3)] The cat needs the squirrel.[(triple4 OR ((triple11) -> rule5) OR ((triple16) -> rule5))] The cow eats the squirrel.[(triple5)] The cow is green.[(triple6)] The cow is not rough.[(triple7)] The cow is young.[(triple8)] The cow needs the cat.[(triple9)] The cow needs the squirrel.[(triple10 OR ((triple9) -> rule4))] The cow sees the cat.[(triple11)] The squirrel eats the cat.[(triple12)] The squirrel is red.[(triple13 OR ((triple12) -> rule3))] The squirrel needs the cat.[(triple14)] The squirrel sees the bald eagle.[(triple15)] The squirrel sees the cat.[(triple16)] @1: The squirrel needs the squirrel.[(((triple14) -> rule4))]
The bald eagle is not green.
("bald eagle" "is" "green" "-")
triple1
The bald eagle is red.
("bald eagle" "is" "red" "+")
triple2
The cat is red.
("cat" "is" "red" "+")
triple3
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
triple4
((triple11) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
((triple16) -> (rule5 % int1))
The cat needs the squirrel.
("cat" "needs" "squirrel" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The cow is not rough.
("cow" "is" "rough" "-")
triple7
The cow is young.
("cow" "is" "young" "+")
triple8
The cow needs the cat.
("cow" "needs" "cat" "+")
triple9
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple10
((triple9) -> (rule4 % int1))
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
int1
The cow sees the cat.
("cow" "sees" "cat" "+")
triple11
The squirrel eats the cat.
("squirrel" "eats" "cat" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
triple13
((triple12) -> (rule3 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel needs the cat.
("squirrel" "needs" "cat" "+")
triple14
The squirrel sees the bald eagle.
("squirrel" "sees" "bald eagle" "+")
triple15
The squirrel sees the cat.
("squirrel" "sees" "cat" "+")
triple16
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
((triple14) -> (rule4 % int1))
The squirrel needs the squirrel.
("squirrel" "needs" "squirrel" "+")
int1