The tiger is big. The tiger is cold. The tiger is nice. The tiger is round. The tiger is young. Young, cold people are nice. Nice people are young. If the tiger is young then the tiger is cold. If someone is nice and big then they are round. If the tiger is cold and the tiger is round then the tiger is big. If the tiger is cold and the tiger is round then the tiger is nice. If the tiger is nice and the tiger is big then the tiger is round. All young people are big.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
Young, cold people are nice.
((("someone" "is" "young" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
Nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If the tiger is young then the tiger is cold.
((("tiger" "is" "young" "+")) -> ("tiger" "is" "cold" "+"))
If someone is nice and big then they are round.
((("someone" "is" "nice" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If the tiger is cold and the tiger is round then the tiger is big.
((("tiger" "is" "cold" "+") ("tiger" "is" "round" "+")) -> ("tiger" "is" "big" "+"))
If the tiger is cold and the tiger is round then the tiger is nice.
((("tiger" "is" "cold" "+") ("tiger" "is" "round" "+")) -> ("tiger" "is" "nice" "+"))
If the tiger is nice and the tiger is big then the tiger is round.
((("tiger" "is" "nice" "+") ("tiger" "is" "big" "+")) -> ("tiger" "is" "round" "+"))
All young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
The tiger is young.
True
1
proof
[(triple5 OR ((triple3) -> rule2) OR ((((triple2 triple4) -> rule6)) -> rule2))]
("tiger" "is" "young" "+")
triple5
((triple3) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple2 triple4) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is not cold.
False
1
inv-proof
[(triple2 OR ((triple5) -> rule3) OR ((((triple3) -> rule2)) -> rule3))]
("tiger" "is" "cold" "-")
triple2
((triple5) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "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 ((triple5) -> rule8) OR ((triple2 triple4) -> rule5) OR ((((triple3) -> rule2)) -> rule8) OR ((((triple5) -> rule3) triple4) -> rule5) OR ((((((triple2 triple4) -> rule6)) -> rule2)) -> rule8) OR ((((((triple3) -> rule2)) -> rule3) triple4) -> rule5))] The tiger is cold.[(triple2 OR ((triple5) -> rule3) OR ((((triple3) -> rule2)) -> rule3))] The tiger is nice.[(triple3 OR ((triple2 triple4) -> rule6) OR ((triple5 triple2) -> rule1) OR ((triple5 ((triple5) -> rule3)) -> rule1) OR ((((triple5) -> rule3) triple4) -> rule6))] The tiger is round.[(triple4 OR ((triple3 triple1) -> rule4) OR ((triple3 triple1) -> rule7) OR ((triple3 ((triple5) -> rule8)) -> rule4) OR ((triple3 ((triple5) -> rule8)) -> rule7) OR ((((triple5 triple2) -> rule1) triple1) -> rule4) OR ((((triple5 triple2) -> rule1) triple1) -> rule7) OR ((((triple5 triple2) -> rule1) ((triple5) -> rule8)) -> rule4) OR ((((triple5 triple2) -> rule1) ((triple5) -> rule8)) -> rule7) OR ((triple3 ((((triple3) -> rule2)) -> rule8)) -> rule4) OR ((triple3 ((((triple3) -> rule2)) -> rule8)) -> rule7) OR ((((triple5 ((triple5) -> rule3)) -> rule1) triple1) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule1) triple1) -> rule7) OR ((((triple5 triple2) -> rule1) ((((triple3) -> rule2)) -> rule8)) -> rule4) OR ((((triple5 triple2) -> rule1) ((((triple3) -> rule2)) -> rule8)) -> rule7) OR ((((triple5 ((triple5) -> rule3)) -> rule1) ((triple5) -> rule8)) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule1) ((triple5) -> rule8)) -> rule7) OR ((((triple5 ((triple5) -> rule3)) -> rule1) ((((triple3) -> rule2)) -> rule8)) -> rule4) OR ((((triple5 ((triple5) -> rule3)) -> rule1) ((((triple3) -> rule2)) -> rule8)) -> rule7))] The tiger is young.[(triple5 OR ((triple3) -> rule2) OR ((((triple2 triple4) -> rule6)) -> rule2))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
((triple5) -> (rule8 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((triple2 triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
((((triple5) -> (rule3 % int2)) triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((((triple2 triple4) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((((triple3) -> (rule2 % int3))) -> (rule3 % int2)) triple4) -> (rule5 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
triple2
((triple5) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple3) -> (rule2 % int2))) -> (rule3 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is young.
("tiger" "is" "young" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
((triple2 triple4) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple5 triple2) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((triple5 ((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((triple5) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is round.
("tiger" "is" "round" "+")
triple4
((triple3 triple1) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((triple3 triple1) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
((triple3 ((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((triple3 ((triple5) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
((((triple5 triple2) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple5 triple2) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
((((triple5 triple2) -> (rule1 % int3)) ((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((((triple5 triple2) -> (rule1 % int3)) ((triple5) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((triple3 ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple5 ((triple5) -> (rule3 % int3))) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
int3
((((triple5 triple2) -> (rule1 % int4)) ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
((((triple5 triple2) -> (rule1 % int4)) ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
((((triple5 ((triple5) -> (rule3 % int4))) -> (rule1 % int3)) ((triple5) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
((((triple5 ((triple5) -> (rule3 % int4))) -> (rule1 % int3)) ((triple5) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
int3
The tiger is cold.
("tiger" "is" "cold" "+")
int4
((((triple5 ((triple5) -> (rule3 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
int5
((((triple5 ((triple5) -> (rule3 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The tiger is round.
("tiger" "is" "round" "+")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is young.
("tiger" "is" "young" "+")
int3
The tiger is nice.
("tiger" "is" "nice" "+")
int4
The tiger is cold.
("tiger" "is" "cold" "+")
int5
The tiger is young.
("tiger" "is" "young" "+")
triple5
((triple3) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
((((triple2 triple4) -> (rule6 % int2))) -> (rule2 % int1))
The tiger is young.
("tiger" "is" "young" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2