The squirrel chases the tiger. The squirrel does not eat the tiger. The squirrel is big. The squirrel is blue. The squirrel is kind. The squirrel is red. The squirrel is round. The squirrel does not visit the tiger. The tiger chases the squirrel. The tiger eats the squirrel. The tiger is big. The tiger is not blue. The tiger is kind. The tiger is red. The tiger is round. The tiger visits the squirrel. If someone eats the tiger and they chase the tiger then they are red. If someone eats the tiger and they are round then they visit the tiger. If someone chases the tiger then the tiger is kind. If the tiger eats the squirrel and the squirrel is not big then the tiger chases the squirrel. If someone eats the squirrel and they do not eat the tiger then the tiger is not blue. If someone is blue then they visit the squirrel. If the squirrel eats the tiger and the squirrel chases the tiger then the squirrel is red. If someone visits the squirrel and they are kind then they chase the squirrel.
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
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 is round.
("squirrel" "is" "round" "+")
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not blue.
("tiger" "is" "blue" "-")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone eats the tiger and they chase the tiger then they are red.
((("someone" "eats" "tiger" "+") ("someone" "chases" "tiger" "+")) -> ("someone" "is" "red" "+"))
If someone eats the tiger and they are round then they visit the tiger.
((("someone" "eats" "tiger" "+") ("someone" "is" "round" "+")) -> ("someone" "visits" "tiger" "+"))
If someone chases the tiger then the tiger is kind.
((("someone" "chases" "tiger" "+")) -> ("tiger" "is" "kind" "+"))
If the tiger eats the squirrel and the squirrel is not big then the tiger chases the squirrel.
((("tiger" "eats" "squirrel" "+") ("squirrel" "is" "big" "~")) -> ("tiger" "chases" "squirrel" "+"))
If someone eats the squirrel and they do not eat the tiger then the tiger is not blue.
((("someone" "eats" "squirrel" "+") ("someone" "eats" "tiger" "~")) -> ("tiger" "is" "blue" "-"))
If someone is blue then they visit the squirrel.
((("someone" "is" "blue" "+")) -> ("someone" "visits" "squirrel" "+"))
If the squirrel eats the tiger and the squirrel chases the tiger then the squirrel is red.
((("squirrel" "eats" "tiger" "+") ("squirrel" "chases" "tiger" "+")) -> ("squirrel" "is" "red" "+"))
If someone visits the squirrel and they are kind then they chase the squirrel.
((("someone" "visits" "squirrel" "+") ("someone" "is" "kind" "+")) -> ("someone" "chases" "squirrel" "+"))
The tiger is kind.
True
1
proof
[(triple13 OR ((triple1) -> rule3))]
("tiger" "is" "kind" "+")
triple13
((triple1) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The squirrel eats the tiger.
False
1
inv-proof
[(triple2)]
("squirrel" "eats" "tiger" "+")
triple2
The squirrel visits the squirrel.
True
2
proof
[(((triple4) -> rule6))]
("squirrel" "visits" "squirrel" "+")
((triple4) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel does not visit the squirrel.
False
2
inv-proof
[(((triple4) -> rule6))]
("squirrel" "visits" "squirrel" "-")
((triple4) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the squirrel.
True
4
proof
[(((((triple4) -> rule6) triple5) -> rule8))]
("squirrel" "chases" "squirrel" "+")
((((triple4) -> (rule6 % int2)) triple5) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The squirrel does not chase the squirrel.
False
4
inv-proof
[(((((triple4) -> rule6) triple5) -> rule8))]
("squirrel" "chases" "squirrel" "-")
((((triple4) -> (rule6 % int2)) triple5) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2
The tiger does not visit the tiger.
Unknown
inv-rconc
[@1: The tiger visits the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "visits" "tiger" "-")
The tiger chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
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 tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The squirrel chases the tiger.[(triple1)] The squirrel does not eat the tiger.[(triple2)] The squirrel does not visit the tiger.[(triple8)] The squirrel is big.[(triple3)] The squirrel is blue.[(triple4)] The squirrel is kind.[(triple5)] The squirrel is red.[(triple6)] The squirrel is round.[(triple7)] The tiger chases the squirrel.[(triple9 OR ((triple16 triple13) -> rule8) OR ((triple16 ((triple1) -> rule3)) -> rule8))] The tiger eats the squirrel.[(triple10)] The tiger is big.[(triple11)] The tiger is kind.[(triple13 OR ((triple1) -> rule3))] The tiger is not blue.[(triple12)] The tiger is red.[(triple14)] The tiger is round.[(triple15)] The tiger visits the squirrel.[(triple16)] @1: The squirrel visits the squirrel.[(((triple4) -> rule6))] @2: The squirrel chases the squirrel.[(((((triple4) -> rule6) triple5) -> rule8))]
The squirrel chases the tiger.
("squirrel" "chases" "tiger" "+")
triple1
The squirrel does not eat the tiger.
("squirrel" "eats" "tiger" "-")
triple2
The squirrel does not visit the tiger.
("squirrel" "visits" "tiger" "-")
triple8
The squirrel is big.
("squirrel" "is" "big" "+")
triple3
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple4
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple5
The squirrel is red.
("squirrel" "is" "red" "+")
triple6
The squirrel is round.
("squirrel" "is" "round" "+")
triple7
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
triple9
((triple16 triple13) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
((triple16 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger is kind.
("tiger" "is" "kind" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
triple10
The tiger is big.
("tiger" "is" "big" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple13
((triple1) -> (rule3 % int1))
The tiger is kind.
("tiger" "is" "kind" "+")
int1
The tiger is not blue.
("tiger" "is" "blue" "-")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple14
The tiger is round.
("tiger" "is" "round" "+")
triple15
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple16
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
((triple4) -> (rule6 % int1))
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int1
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
((((triple4) -> (rule6 % int2)) triple5) -> (rule8 % int1))
The squirrel chases the squirrel.
("squirrel" "chases" "squirrel" "+")
int1
The squirrel visits the squirrel.
("squirrel" "visits" "squirrel" "+")
int2