The cat is red. The mouse likes the squirrel. The squirrel does not need the mouse. The tiger needs the mouse. If something likes the squirrel then it sees the squirrel. If the squirrel is cold and the squirrel likes the tiger then the tiger needs the mouse. If something sees the mouse and the mouse does not see the squirrel then it is cold.
The cat is red.
("cat" "is" "red" "+")
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something likes the squirrel then it sees the squirrel.
((("something" "likes" "squirrel" "+")) -> ("something" "sees" "squirrel" "+"))
If the squirrel is cold and the squirrel likes the tiger then the tiger needs the mouse.
((("squirrel" "is" "cold" "+") ("squirrel" "likes" "tiger" "+")) -> ("tiger" "needs" "mouse" "+"))
If something sees the mouse and the mouse does not see the squirrel then it is cold.
((("something" "sees" "mouse" "+") ("mouse" "sees" "squirrel" "~")) -> ("something" "is" "cold" "+"))
The tiger needs the mouse.
True
1
proof
[(triple4)]
("tiger" "needs" "mouse" "+")
triple4
The tiger does not need the mouse.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "mouse" "-")
triple4
The mouse sees the squirrel.
True
2
proof
[(((triple2) -> rule1))]
("mouse" "sees" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The mouse does not see the squirrel.
False
2
inv-proof
[(((triple2) -> rule1))]
("mouse" "sees" "squirrel" "-")
((triple2) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1
The squirrel is not cold.
Unknown
inv-rconc
[@1: The squirrel is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("squirrel" "is" "cold" "-")
The squirrel sees the squirrel.
Unknown
rconc
[@1: The squirrel sees the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "sees" "squirrel" "+")
The mouse does not need the squirrel.
Unknown
inv-random
[@0: The mouse needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "needs" "squirrel" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat is red.[(triple1)] The mouse likes the squirrel.[(triple2)] The squirrel does not need the mouse.[(triple3)] The tiger needs the mouse.[(triple4)] @1: The mouse sees the squirrel.[(((triple2) -> rule1))]
The cat is red.
("cat" "is" "red" "+")
triple1
The mouse likes the squirrel.
("mouse" "likes" "squirrel" "+")
triple2
The squirrel does not need the mouse.
("squirrel" "needs" "mouse" "-")
triple3
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple4
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
((triple2) -> (rule1 % int1))
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
int1