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