The tiger is big. The tiger is green. The tiger is nice. The tiger is red. The tiger is rough. If something is rough then it is red. If the tiger is rough then the tiger is big. All big things are rough. If the tiger is big then the tiger is rough. If something is nice and not rough then it is green. Nice things are green.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
If something is rough then it is red.
((("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If the tiger is rough then the tiger is big.
((("tiger" "is" "rough" "+")) -> ("tiger" "is" "big" "+"))
All big things are rough.
((("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
If the tiger is big then the tiger is rough.
((("tiger" "is" "big" "+")) -> ("tiger" "is" "rough" "+"))
If something is nice and not rough then it is green.
((("something" "is" "nice" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
Nice things are green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
The tiger is red.
True
1
proof
[(triple4 OR ((triple5) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule4)) -> rule1))]
("tiger" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is not nice.
False
1
inv-proof
[(triple3)]
("tiger" "is" "nice" "-")
triple3
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 chases the tiger.
Unknown
random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "+")
@0: The tiger is big.[(triple1 OR ((triple5) -> rule2))] The tiger is green.[(triple2 OR ((triple3) -> rule6))] The tiger is nice.[(triple3)] The tiger is red.[(triple4 OR ((triple5) -> rule1) OR ((((triple1) -> rule3)) -> rule1) OR ((((triple1) -> rule4)) -> rule1))] The tiger is rough.[(triple5 OR ((triple1) -> rule3) OR ((triple1) -> rule4))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
((triple5) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
triple2
((triple3) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
The tiger is red.
("tiger" "is" "red" "+")
triple4
((triple5) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
((((triple1) -> (rule4 % int2))) -> (rule1 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
triple5
((triple1) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((triple1) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1