The bear is red. The mouse eats the squirrel. The squirrel eats the tiger. The tiger does not visit the bear. If someone eats the tiger then they like the mouse. If someone likes the mouse then the mouse eats the tiger.
The bear is red.
("bear" "is" "red" "+")
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
If someone eats the tiger then they like the mouse.
((("someone" "eats" "tiger" "+")) -> ("someone" "likes" "mouse" "+"))
If someone likes the mouse then the mouse eats the tiger.
((("someone" "likes" "mouse" "+")) -> ("mouse" "eats" "tiger" "+"))
The bear is red.
True
1
proof
[(triple1)]
("bear" "is" "red" "+")
triple1
The mouse does not eat the squirrel.
False
1
inv-proof
[(triple2)]
("mouse" "eats" "squirrel" "-")
triple2
The squirrel likes the mouse.
True
2
proof
[(((triple3) -> rule1))]
("squirrel" "likes" "mouse" "+")
((triple3) -> (rule1 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The squirrel does not like the mouse.
False
2
inv-proof
[(((triple3) -> rule1))]
("squirrel" "likes" "mouse" "-")
((triple3) -> (rule1 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse eats the tiger.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "eats" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("mouse" "eats" "tiger" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse likes the mouse.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int3
The mouse does not like the mouse.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
("mouse" "likes" "mouse" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int3
The bear does not like the mouse.
Unknown
inv-rconc
[@1: The bear likes the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "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 mouse does not visit the bear.
Unknown
inv-random
[@0: The mouse visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "bear" "-")
The squirrel is blue.
Unknown
random
[@0: The squirrel is blue.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "blue" "+")
The tiger does not eat the squirrel.
Unknown
inv-random
[@0: The tiger eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "squirrel" "-")
The squirrel visits the bear.
Unknown
random
[@0: The squirrel visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "bear" "+")
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The mouse visits the mouse.
Unknown
random
[@0: The mouse visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "mouse" "+")
@0: The bear is red.[(triple1)] The mouse eats the squirrel.[(triple2)] The squirrel eats the tiger.[(triple3)] The tiger does not visit the bear.[(triple4)] @1: The squirrel likes the mouse.[(((triple3) -> rule1))] @2: The mouse eats the tiger.[(((((triple3) -> rule1)) -> rule2))] @3: The mouse likes the mouse.[(((((((triple3) -> rule1)) -> rule2)) -> rule1))]
The bear is red.
("bear" "is" "red" "+")
triple1
The mouse eats the squirrel.
("mouse" "eats" "squirrel" "+")
triple2
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple3
The tiger does not visit the bear.
("tiger" "visits" "bear" "-")
triple4
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
((triple3) -> (rule1 % int1))
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int1
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int2
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The mouse likes the mouse.
("mouse" "likes" "mouse" "+")
int1
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
int2
The squirrel likes the mouse.
("squirrel" "likes" "mouse" "+")
int3