The squirrel is big. The squirrel is green. The squirrel is kind. The squirrel is red. The squirrel needs the tiger. The squirrel does not see the tiger. The squirrel visits the tiger. The tiger is red. The tiger is round. The tiger needs the squirrel. The tiger sees the squirrel. The tiger visits the squirrel. If something sees the squirrel and the squirrel does not visit the tiger then the squirrel needs the tiger. If something sees the squirrel and the squirrel is not round then the squirrel needs the tiger. If something is green and it does not need the squirrel then the squirrel does not need the tiger. If something needs the squirrel then the squirrel is kind. If the tiger is round and the tiger is not red then the tiger visits the squirrel. If something visits the tiger then the tiger sees the squirrel. If the tiger visits the squirrel and the tiger does not need the squirrel then the tiger does not see the squirrel. If something is big and it does not see the squirrel then it does not need the tiger.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If something sees the squirrel and the squirrel does not visit the tiger then the squirrel needs the tiger.
((("something" "sees" "squirrel" "+") ("squirrel" "visits" "tiger" "~")) -> ("squirrel" "needs" "tiger" "+"))
If something sees the squirrel and the squirrel is not round then the squirrel needs the tiger.
((("something" "sees" "squirrel" "+") ("squirrel" "is" "round" "~")) -> ("squirrel" "needs" "tiger" "+"))
If something is green and it does not need the squirrel then the squirrel does not need the tiger.
((("something" "is" "green" "+") ("something" "needs" "squirrel" "~")) -> ("squirrel" "needs" "tiger" "-"))
If something needs the squirrel then the squirrel is kind.
((("something" "needs" "squirrel" "+")) -> ("squirrel" "is" "kind" "+"))
If the tiger is round and the tiger is not red then the tiger visits the squirrel.
((("tiger" "is" "round" "+") ("tiger" "is" "red" "~")) -> ("tiger" "visits" "squirrel" "+"))
If something visits the tiger then the tiger sees the squirrel.
((("something" "visits" "tiger" "+")) -> ("tiger" "sees" "squirrel" "+"))
If the tiger visits the squirrel and the tiger does not need the squirrel then the tiger does not see the squirrel.
((("tiger" "visits" "squirrel" "+") ("tiger" "needs" "squirrel" "~")) -> ("tiger" "sees" "squirrel" "-"))
If something is big and it does not see the squirrel then it does not need the tiger.
((("something" "is" "big" "+") ("something" "sees" "squirrel" "~")) -> ("something" "needs" "tiger" "-"))
The tiger visits the squirrel.
True
1
proof
[(triple12)]
("tiger" "visits" "squirrel" "+")
triple12
The tiger does not see the squirrel.
False
1
inv-proof
[(triple11 OR ((triple7) -> rule6))]
("tiger" "sees" "squirrel" "-")
triple11
((triple7) -> (rule6 % int1))
The tiger sees the squirrel.
("tiger" "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 squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The squirrel does not see the tiger.[(triple6)] The squirrel is big.[(triple1)] The squirrel is green.[(triple2)] The squirrel is kind.[(triple3 OR ((triple10) -> rule4))] The squirrel is red.[(triple4)] The squirrel needs the tiger.[(triple5)] The squirrel visits the tiger.[(triple7)] The tiger is red.[(triple8)] The tiger is round.[(triple9)] The tiger needs the squirrel.[(triple10)] The tiger sees the squirrel.[(triple11 OR ((triple7) -> rule6))] The tiger visits the squirrel.[(triple12)]
The squirrel does not see the tiger.
("squirrel" "sees" "tiger" "-")
triple6
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
((triple10) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
The squirrel needs the tiger.
("squirrel" "needs" "tiger" "+")
triple5
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple7
The tiger is red.
("tiger" "is" "red" "+")
triple8
The tiger is round.
("tiger" "is" "round" "+")
triple9
The tiger needs the squirrel.
("tiger" "needs" "squirrel" "+")
triple10
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
triple11
((triple7) -> (rule6 % int1))
The tiger sees the squirrel.
("tiger" "sees" "squirrel" "+")
int1
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple12