The tiger is blue. The tiger is nice. The tiger is young. If the tiger is big and the tiger is rough then the tiger is young. Blue people are nice. If someone is young and nice then they are rough. All blue people are big. Big, nice people are rough. If someone is young then they are nice.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is young.
("tiger" "is" "young" "+")
If the tiger is big and the tiger is rough then the tiger is young.
((("tiger" "is" "big" "+") ("tiger" "is" "rough" "+")) -> ("tiger" "is" "young" "+"))
Blue people are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is young and nice then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
All blue people are big.
((("someone" "is" "blue" "+")) -> ("someone" "is" "big" "+"))
Big, nice people are rough.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
The tiger is nice.
True
1
proof
[(triple2 OR ((triple1) -> rule2) OR ((triple3) -> rule6))]
("tiger" "is" "nice" "+")
triple2
((triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is not blue.
False
1
inv-proof
[(triple1)]
("tiger" "is" "blue" "-")
triple1
The tiger is big.
True
2
proof
[(((triple1) -> rule4))]
("tiger" "is" "big" "+")
((triple1) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
2
inv-proof
[(((triple1) -> rule4))]
("tiger" "is" "big" "-")
((triple1) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
@0: The tiger is blue.[(triple1)] The tiger is nice.[(triple2 OR ((triple1) -> rule2) OR ((triple3) -> rule6))] The tiger is young.[(triple3 OR ((((triple1) -> rule4) ((((triple1) -> rule4) triple2) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule5)) -> rule1))] @1: The tiger is big.[(((triple1) -> rule4))] The tiger is rough.[(((triple3 triple2) -> rule3) OR ((triple3 ((triple1) -> rule2)) -> rule3) OR ((triple3 ((triple3) -> rule6)) -> rule3) OR ((((triple1) -> rule4) triple2) -> rule5) OR ((((triple1) -> rule4) ((triple1) -> rule2)) -> rule5) OR ((((triple1) -> rule4) ((triple3) -> rule6)) -> rule5))]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
((triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple3) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
triple3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple2) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((triple1) -> (rule4 % int4)) ((((triple1) -> (rule4 % int4)) ((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule1 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger is big.
("tiger" "is" "big" "+")
((triple1) -> (rule4 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple3 triple2) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
((triple3 ((triple1) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((triple3 ((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple1) -> (rule4 % int2)) triple2) -> (rule5 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple1) -> (rule4 % int3)) ((triple1) -> (rule2 % int2))) -> (rule5 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((triple1) -> (rule4 % int3)) ((triple3) -> (rule6 % int2))) -> (rule5 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3