The cow is rough. The cow visits the tiger. The mouse visits the cow. The squirrel eats the mouse. The squirrel eats the tiger. The squirrel is nice. The squirrel needs the cow. The squirrel needs the mouse. The squirrel visits the mouse. The tiger eats the squirrel. If something needs the tiger then it visits the mouse. If something visits the cow then it visits the squirrel. If something visits the tiger then the tiger visits the cow.
The cow is rough.
("cow" "is" "rough" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
If something needs the tiger then it visits the mouse.
((("something" "needs" "tiger" "+")) -> ("something" "visits" "mouse" "+"))
If something visits the cow then it visits the squirrel.
((("something" "visits" "cow" "+")) -> ("something" "visits" "squirrel" "+"))
If something visits the tiger then the tiger visits the cow.
((("something" "visits" "tiger" "+")) -> ("tiger" "visits" "cow" "+"))
The squirrel eats the tiger.
True
1
proof
[(triple5)]
("squirrel" "eats" "tiger" "+")
triple5
The cow is not rough.
False
1
inv-proof
[(triple1)]
("cow" "is" "rough" "-")
triple1
The tiger visits the cow.
True
2
proof
[(((triple2) -> rule3))]
("tiger" "visits" "cow" "+")
((triple2) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger does not visit the cow.
False
2
inv-proof
[(((triple2) -> rule3))]
("tiger" "visits" "cow" "-")
((triple2) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the squirrel.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("tiger" "visits" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The tiger does not visit the squirrel.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("tiger" "visits" "squirrel" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2
The mouse does not visit the mouse.
Unknown
inv-rconc
[@1: The mouse visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "visits" "mouse" "-")
The cow visits the mouse.
Unknown
rconc
[@1: The cow visits the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "visits" "mouse" "+")
The cow does not visit the squirrel.
Unknown
inv-rconc
[@1: The cow visits the squirrel.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "squirrel" "-")
The cow eats the squirrel.
Unknown
random
[@0: The cow eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "squirrel" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow is rough.[(triple1)] The cow visits the tiger.[(triple2)] The mouse visits the cow.[(triple3)] The squirrel eats the mouse.[(triple4)] The squirrel eats the tiger.[(triple5)] The squirrel is nice.[(triple6)] The squirrel needs the cow.[(triple7)] The squirrel needs the mouse.[(triple8)] The squirrel visits the mouse.[(triple9)] The tiger eats the squirrel.[(triple10)] @1: The mouse visits the squirrel.[(((triple3) -> rule2))] The tiger visits the cow.[(((triple2) -> rule3))] @2: The tiger visits the squirrel.[(((((triple2) -> rule3)) -> rule2))]
The cow is rough.
("cow" "is" "rough" "+")
triple1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple2
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple3
The squirrel eats the mouse.
("squirrel" "eats" "mouse" "+")
triple4
The squirrel eats the tiger.
("squirrel" "eats" "tiger" "+")
triple5
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple6
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple7
The squirrel needs the mouse.
("squirrel" "needs" "mouse" "+")
triple8
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple9
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple10
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
((triple3) -> (rule2 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
((triple2) -> (rule3 % int1))
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
int1
The tiger visits the cow.
("tiger" "visits" "cow" "+")
int2