The tiger is blue. The tiger is nice. The tiger is rough. Rough things are nice. All big, blue things are nice. If something is nice and not rough then it is green. All rough things are green. If something is nice then it is blue. All green, blue things are big.
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
Rough things are nice.
((("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
All big, blue things are nice.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If something is nice and not rough then it is green.
((("something" "is" "nice" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
All rough things are green.
((("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is blue.
((("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All green, blue things are big.
((("something" "is" "green" "+") ("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
The tiger is nice.
True
1
proof
[(triple2 OR ((triple3) -> rule1) OR ((((((triple3) -> rule4) triple1) -> rule6) triple1) -> rule2))]
("tiger" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((((triple3) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is not nice.
False
1
inv-proof
[(triple2 OR ((triple3) -> rule1) OR ((((((triple3) -> rule4) triple1) -> rule6) triple1) -> rule2))]
("tiger" "is" "nice" "-")
triple2
((triple3) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((((triple3) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is green.
True
2
proof
[(((triple3) -> rule4))]
("tiger" "is" "green" "+")
((triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is not green.
False
2
inv-proof
[(((triple3) -> rule4))]
("tiger" "is" "green" "-")
((triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
True
4
proof
[(((((triple3) -> rule4) triple1) -> rule6) OR ((((triple3) -> rule4) ((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4) ((((triple3) -> rule1)) -> rule5)) -> rule6))]
("tiger" "is" "big" "+")
((((triple3) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The tiger is not big.
False
4
inv-proof
[(((((triple3) -> rule4) triple1) -> rule6) OR ((((triple3) -> rule4) ((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4) ((((triple3) -> rule1)) -> rule5)) -> rule6))]
("tiger" "is" "big" "-")
((((triple3) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The tiger does not visit the tiger.
Unknown
inv-random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "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 OR ((triple2) -> rule5) OR ((((triple3) -> rule1)) -> rule5))] The tiger is nice.[(triple2 OR ((triple3) -> rule1) OR ((((((triple3) -> rule4) triple1) -> rule6) triple1) -> rule2))] The tiger is rough.[(triple3)] @1: The tiger is green.[(((triple3) -> rule4))] @2: The tiger is big.[(((((triple3) -> rule4) triple1) -> rule6) OR ((((triple3) -> rule4) ((triple2) -> rule5)) -> rule6) OR ((((triple3) -> rule4) ((((triple3) -> rule1)) -> rule5)) -> rule6))]
The tiger is blue.
("tiger" "is" "blue" "+")
triple1
((triple2) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule5 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
((triple3) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((((triple3) -> (rule4 % int3)) triple1) -> (rule6 % int2)) triple1) -> (rule2 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
((triple3) -> (rule4 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
((((triple3) -> (rule4 % int2)) triple1) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple3) -> (rule4 % int3)) ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is green.
("tiger" "is" "green" "+")
int3
((((triple3) -> (rule4 % int4)) ((((triple3) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4