The bear sees the squirrel. The cow is young. The mouse needs the cow. The squirrel needs the mouse. If something is red then it is young. If something needs the cow then it is not young. If something is cold then it is blue.
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
The cow is young.
("cow" "is" "young" "+")
The mouse needs the cow.
("mouse" "needs" "cow" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something needs the cow then it is not young.
((("something" "needs" "cow" "+")) -> ("something" "is" "young" "-"))
If something is cold then it is blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
The squirrel needs the mouse.
True
1
proof
[(triple4)]
("squirrel" "needs" "mouse" "+")
triple4
The cow is not young.
False
1
inv-proof
[(triple2)]
("cow" "is" "young" "-")
triple2
The mouse is not young.
True
2
proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "-")
((triple3) -> (rule2 % int1))
The mouse is not young.
("mouse" "is" "young" "-")
int1
The mouse is young.
False
2
inv-proof
[(((triple3) -> rule2))]
("mouse" "is" "young" "+")
((triple3) -> (rule2 % int1))
The mouse is not young.
("mouse" "is" "young" "-")
int1
The bear is not young.
Unknown
inv-rconc
[@1: The bear is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "young" "-")
The squirrel is blue.
Unknown
rconc
[@1: The squirrel is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "blue" "+")
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 cow needs the squirrel.
Unknown
random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "+")
@0: The bear sees the squirrel.[(triple1)] The cow is young.[(triple2)] The mouse needs the cow.[(triple3)] The squirrel needs the mouse.[(triple4)] @1: The mouse is not young.[(((triple3) -> rule2))]
The bear sees the squirrel.
("bear" "sees" "squirrel" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The mouse needs the cow.
("mouse" "needs" "cow" "+")
triple3
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple4
The mouse is not young.
("mouse" "is" "young" "-")
((triple3) -> (rule2 % int1))
The mouse is not young.
("mouse" "is" "young" "-")
int1