The squirrel chases the tiger. The squirrel is cold. The squirrel is kind. The squirrel is rough. The squirrel is round. The squirrel sees the tiger. The squirrel visits the tiger. The tiger chases the squirrel. The tiger is blue. The tiger is cold. The tiger is kind. The tiger is rough. The tiger is round. The tiger sees the squirrel. The tiger visits the squirrel. If someone is round then they see the squirrel. If someone visits the squirrel and the squirrel chases the tiger then the tiger chases the squirrel.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel is cold.
("squirrel" "is" "cold" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is rough.
("squirrel" "is" "rough" "+")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone is round then they see the squirrel.
((("someone" "is" "round" "+")) -> ("someone" "sees" "squirrel" "+"))
If someone visits the squirrel and the squirrel chases the tiger then the tiger chases the squirrel.
((("someone" "visits" "squirrel" "+") ("squirrel" "chases" "tiger" "+")) -> ("tiger" "chases" "squirrel" "+"))
The squirrel sees the tiger.
True
1
proof
[(triple6)]
("squirrel" "sees" "tiger" "+")
triple6
The tiger does not see the squirrel.
False
1
inv-proof
[(triple14 OR ((triple13) -> rule1))]
("tiger" "sees" "squirrel" "-")
triple14
((triple13) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The squirrel sees the squirrel.
True
2
proof
[(((triple5) -> rule1))]
("squirrel" "sees" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The squirrel does not see the squirrel.
False
2
inv-proof
[(((triple5) -> rule1))]
("squirrel" "sees" "squirrel" "-")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1
The tiger does not see the tiger.
Unknown
inv-random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The squirrel chases the tiger.[(triple1)] The squirrel is cold.[(triple2)] The squirrel is kind.[(triple3)] The squirrel is rough.[(triple4)] The squirrel is round.[(triple5)] The squirrel sees the tiger.[(triple6)] The squirrel visits the tiger.[(triple7)] The tiger chases the squirrel.[(triple8 OR ((triple15 triple1) -> rule2))] The tiger is blue.[(triple9)] The tiger is cold.[(triple10)] The tiger is kind.[(triple11)] The tiger is rough.[(triple12)] The tiger is round.[(triple13)] The tiger sees the squirrel.[(triple14 OR ((triple13) -> rule1))] The tiger visits the squirrel.[(triple15)] @1: The squirrel sees the squirrel.[(((triple5) -> rule1))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel is cold.
("squirrel" "is" "cold" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple4
The squirrel is round.
("squirrel" "is" "round" "+")
triple5
The squirrel sees the tiger.
("squirrel" "sees" "tiger" "+")
triple6
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple8
((triple15 triple1) -> (rule2 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple9
The tiger is cold.
("tiger" "is" "cold" "+")
triple10
The tiger is kind.
("tiger" "is" "kind" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple14
((triple13) -> (rule1 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple15
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
((triple5) -> (rule1 % int1))
The squirrel sees the squirrel.
("squirrel" "sees" "squirrel" "+")
int1