The tiger is big. The tiger is not red. The tiger is not rough. The tiger is round. The tiger is young. If the tiger is red and the tiger is not big then the tiger is rough. If the tiger is round then the tiger is not rough. If something is big and not young then it is red. All rough things are red. Young things are not rough. If something is red and big then it is rough. If something is red and not young then it is round. Young things are round.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is not red.
("tiger" "is" "red" "-")
The tiger is not rough.
("tiger" "is" "rough" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is red and the tiger is not big then the tiger is rough.
((("tiger" "is" "red" "+") ("tiger" "is" "big" "~")) -> ("tiger" "is" "rough" "+"))
If the tiger is round then the tiger is not rough.
((("tiger" "is" "round" "+")) -> ("tiger" "is" "rough" "-"))
If something is big and not young then it is red.
((("something" "is" "big" "+") ("something" "is" "young" "~")) -> ("something" "is" "red" "+"))
All rough things are red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
Young things are not rough.
((("something" "is" "young" "+")) -> ("something" "is" "rough" "-"))
If something is red and big then it is rough.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If something is red and not young then it is round.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "round" "+"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
The tiger is not rough.
True
1
proof
[(triple3 OR ((triple4) -> rule2) OR ((triple5) -> rule5) OR ((((triple5) -> rule8)) -> rule2))]
("tiger" "is" "rough" "-")
triple3
((triple4) -> (rule2 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
((triple5) -> (rule5 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is not young.
False
1
inv-proof
[(triple5)]
("tiger" "is" "young" "-")
triple5
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The tiger is big.[(triple1)] The tiger is not red.[(triple2)] The tiger is not rough.[(triple3 OR ((triple4) -> rule2) OR ((triple5) -> rule5) OR ((((triple5) -> rule8)) -> rule2))] The tiger is round.[(triple4 OR ((triple5) -> rule8))] The tiger is young.[(triple5)]
The tiger is big.
("tiger" "is" "big" "+")
triple1
The tiger is not red.
("tiger" "is" "red" "-")
triple2
The tiger is not rough.
("tiger" "is" "rough" "-")
triple3
((triple4) -> (rule2 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
((triple5) -> (rule5 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
((((triple5) -> (rule8 % int2))) -> (rule2 % int1))
The tiger is not rough.
("tiger" "is" "rough" "-")
int1
The tiger is round.
("tiger" "is" "round" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
triple4
((triple5) -> (rule8 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
triple5