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