The tiger is big. The tiger is not green. The tiger is not nice. The tiger is rough. The tiger is round. If someone is green and round then they are nice. If someone is big and green then they are nice. Green people are not nice. All nice people are rough. If the tiger is green and the tiger is rough then the tiger is nice. All round, nice people are not green. If someone is round and not big then they are green. If the tiger is round then the tiger is rough.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not green.
("tiger" "is" "green" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
If someone is green and round then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is big and green then they are nice.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
Green people are not nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "-"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If the tiger is green and the tiger is rough then the tiger is nice.
((("tiger" "is" "green" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "is" "nice" "+"))
All round, nice people are not green.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "-"))
If someone is round and not big then they are green.
((("someone" "is" "round" "+") ("someone" "is" "big" "~")) -> ("someone" "is" "green" "+"))
If the tiger is round then the tiger is rough.
((("tiger" "is" "round" "+")) -> ("tiger" "is" "rough" "+"))
The tiger is not green.
True
1
proof
[(triple2)]
("tiger" "is" "green" "-")
triple2
The tiger is not big.
False
1
inv-proof
[(triple1)]
("tiger" "is" "big" "-")
triple1
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The tiger needs the tiger.
Unknown
random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "+")
@0: The tiger is big.[(triple1)] The tiger is not green.[(triple2)] The tiger is not nice.[(triple3)] The tiger is rough.[(triple4 OR ((triple5) -> rule8))] The tiger is round.[(triple5)]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is not green.
("tiger" "is" "green" "-")
triple2
The tiger is not nice.
("tiger" "is" "nice" "-")
triple3
The tiger is rough.
("tiger" "is" "rough" "+")
triple4
((triple5) -> (rule8 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is round.
("tiger" "is" "round" "+")
triple5