The tiger is big. The tiger is blue. The tiger is green. The tiger is red. The tiger is young. Red things are big. Blue things are big. If the tiger is young then the tiger is red. Red, young things are blue. If the tiger is green then the tiger is big. Big things are young. If something is blue then it is big. If something is young then it is green.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is young.
("tiger" "is" "young" "+")
Red things are big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If the tiger is young then the tiger is red.
((("tiger" "is" "young" "+")) -> ("tiger" "is" "red" "+"))
Red, young things are blue.
((("something" "is" "red" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If the tiger is green then the tiger is big.
((("tiger" "is" "green" "+")) -> ("tiger" "is" "big" "+"))
Big things are young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is young then it is green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "+"))
The tiger is big.
True
1
proof
[(triple1 OR ((triple2) -> rule2) OR ((triple2) -> rule7) OR ((triple3) -> rule5) OR ((triple4) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule8)) -> rule5) OR ((((triple4 triple5) -> rule4)) -> rule2) OR ((((triple4 triple5) -> rule4)) -> rule7) OR ((((((triple5) -> rule3) triple5) -> rule4)) -> rule2) OR ((((((triple5) -> rule3) triple5) -> rule4)) -> rule7))]
("tiger" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple2) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple3) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple4) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is not young.
False
1
inv-proof
[(triple5 OR ((triple1) -> rule6) OR ((((triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule7)) -> rule6) OR ((((triple3) -> rule5)) -> rule6) OR ((((triple4) -> rule1)) -> rule6))]
("tiger" "is" "young" "-")
triple5
((triple1) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
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 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 OR ((triple2) -> rule2) OR ((triple2) -> rule7) OR ((triple3) -> rule5) OR ((triple4) -> rule1) OR ((((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule8)) -> rule5) OR ((((triple4 triple5) -> rule4)) -> rule2) OR ((((triple4 triple5) -> rule4)) -> rule7) OR ((((((triple5) -> rule3) triple5) -> rule4)) -> rule2) OR ((((((triple5) -> rule3) triple5) -> rule4)) -> rule7))] The tiger is blue.[(triple2 OR ((triple4 triple5) -> rule4) OR ((triple4 ((triple1) -> rule6)) -> rule4) OR ((((triple5) -> rule3) triple5) -> rule4) OR ((((triple5) -> rule3) ((triple1) -> rule6)) -> rule4) OR ((triple4 ((((triple3) -> rule5)) -> rule6)) -> rule4) OR ((triple4 ((((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule3) triple5) -> rule4) OR ((((triple5) -> rule3) ((((triple3) -> rule5)) -> rule6)) -> rule4) OR ((((triple5) -> rule3) ((((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule3) ((triple1) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule3) ((((triple3) -> rule5)) -> rule6)) -> rule4) OR ((((((triple1) -> rule6)) -> rule3) ((((triple4) -> rule1)) -> rule6)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule6)) -> rule3) triple5) -> rule4) OR ((((((((triple3) -> rule5)) -> rule6)) -> rule3) ((triple1) -> rule6)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule6)) -> rule3) ((((triple3) -> rule5)) -> rule6)) -> rule4) OR ((((((((triple3) -> rule5)) -> rule6)) -> rule3) ((((triple4) -> rule1)) -> rule6)) -> rule4))] The tiger is green.[(triple3 OR ((triple5) -> rule8) OR ((((triple1) -> rule6)) -> rule8) OR ((((((triple2) -> rule2)) -> rule6)) -> rule8) OR ((((((triple2) -> rule7)) -> rule6)) -> rule8) OR ((((((triple4) -> rule1)) -> rule6)) -> rule8))] The tiger is red.[(triple4 OR ((triple5) -> rule3) OR ((((triple1) -> rule6)) -> rule3) OR ((((((triple2) -> rule2)) -> rule6)) -> rule3) OR ((((((triple2) -> rule7)) -> rule6)) -> rule3) OR ((((((triple3) -> rule5)) -> rule6)) -> rule3))] The tiger is young.[(triple5 OR ((triple1) -> rule6) OR ((((triple2) -> rule2)) -> rule6) OR ((((triple2) -> rule7)) -> rule6) OR ((((triple3) -> rule5)) -> rule6) OR ((((triple4) -> rule1)) -> rule6))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
((triple2) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple2) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple3) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple4) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((triple5) -> (rule8 % int2))) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((triple4 triple5) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule2 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
((((((triple5) -> (rule3 % int3)) triple5) -> (rule4 % int2))) -> (rule7 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
((triple4 triple5) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
((triple4 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((triple5) -> (rule3 % int2)) triple5) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
((((triple5) -> (rule3 % int3)) ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
((triple4 ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple4 ((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) triple5) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((triple5) -> (rule3 % int4)) ((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
((((triple5) -> (rule3 % int4)) ((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
int4
((((((triple1) -> (rule6 % int3))) -> (rule3 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((((triple1) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple3) -> (rule5 % int2))) -> (rule6 % int4))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
int4
((((((triple1) -> (rule6 % int4))) -> (rule3 % int3)) ((((triple4) -> (rule1 % int2))) -> (rule6 % int4))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) triple5) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((triple1) -> (rule6 % int3))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
((((((((triple3) -> (rule5 % int4))) -> (rule6 % int3))) -> (rule3 % int2)) ((((triple4) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is big.
("tiger" "is" "big" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
triple3
((triple5) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((((triple4) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is red.
("tiger" "is" "red" "+")
triple4
((triple5) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((((triple2) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((((triple2) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((((((triple3) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is young.
("tiger" "is" "young" "+")
triple5
((triple1) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple2) -> (rule2 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple2) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple3) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2