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