The mouse chases the squirrel. The mouse is big. The mouse is blue. The mouse is kind. The mouse is red. The mouse is round. The mouse sees the squirrel. The mouse visits the squirrel. The squirrel chases the mouse. The squirrel is big. The squirrel is blue. The squirrel is kind. The squirrel is red. The squirrel sees the mouse. The squirrel visits the mouse. If something chases the squirrel then it visits the squirrel. If something is big and it visits the squirrel then it chases the mouse.
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse is red.
("mouse" "is" "red" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
If something chases the squirrel then it visits the squirrel.
((("something" "chases" "squirrel" "+")) -> ("something" "visits" "squirrel" "+"))
If something is big and it visits the squirrel then it chases the mouse.
((("something" "is" "big" "+") ("something" "visits" "squirrel" "+")) -> ("something" "chases" "mouse" "+"))
The mouse is round.
True
1
proof
[(triple6)]
("mouse" "is" "round" "+")
triple6
The mouse does not chase the squirrel.
False
1
inv-proof
[(triple1)]
("mouse" "chases" "squirrel" "-")
triple1
The mouse chases the mouse.
True
3
proof
[(((triple2 triple8) -> rule2) OR ((triple2 ((triple1) -> rule1)) -> rule2))]
("mouse" "chases" "mouse" "+")
((triple2 triple8) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The mouse does not chase the mouse.
False
3
inv-proof
[(((triple2 triple8) -> rule2) OR ((triple2 ((triple1) -> rule1)) -> rule2))]
("mouse" "chases" "mouse" "-")
((triple2 triple8) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2
The squirrel does not visit the squirrel.
Unknown
inv-rconc
[@1: The squirrel visits the squirrel.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("squirrel" "visits" "squirrel" "-")
The mouse sees the mouse.
Unknown
random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "+")
The squirrel does not chase the squirrel.
Unknown
inv-random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "-")
The squirrel is round.
Unknown
random
[@0: The squirrel is round.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "round" "+")
@0: The mouse chases the squirrel.[(triple1)] The mouse is big.[(triple2)] The mouse is blue.[(triple3)] The mouse is kind.[(triple4)] The mouse is red.[(triple5)] The mouse is round.[(triple6)] The mouse sees the squirrel.[(triple7)] The mouse visits the squirrel.[(triple8 OR ((triple1) -> rule1))] The squirrel chases the mouse.[(triple9)] The squirrel is big.[(triple10)] The squirrel is blue.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is red.[(triple13)] The squirrel sees the mouse.[(triple14)] The squirrel visits the mouse.[(triple15)] @1: The mouse chases the mouse.[(((triple2 triple8) -> rule2) OR ((triple2 ((triple1) -> rule1)) -> rule2))]
The mouse chases the squirrel.
("mouse" "chases" "squirrel" "+")
triple1
The mouse is big.
("mouse" "is" "big" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The mouse is kind.
("mouse" "is" "kind" "+")
triple4
The mouse is red.
("mouse" "is" "red" "+")
triple5
The mouse is round.
("mouse" "is" "round" "+")
triple6
The mouse sees the squirrel.
("mouse" "sees" "squirrel" "+")
triple7
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
triple8
((triple1) -> (rule1 % int1))
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int1
The squirrel chases the mouse.
("squirrel" "chases" "mouse" "+")
triple9
The squirrel is big.
("squirrel" "is" "big" "+")
triple10
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is red.
("squirrel" "is" "red" "+")
triple13
The squirrel sees the mouse.
("squirrel" "sees" "mouse" "+")
triple14
The squirrel visits the mouse.
("squirrel" "visits" "mouse" "+")
triple15
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((triple2 triple8) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
((triple2 ((triple1) -> (rule1 % int2))) -> (rule2 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse visits the squirrel.
("mouse" "visits" "squirrel" "+")
int2