The tiger is cold. The tiger is nice. The tiger is red. If the tiger is red then the tiger is cold. Cold people are red. If the tiger is cold then the tiger is big. Round, big people are nice. All red, big people are cold. If someone is nice then they are red. If the tiger is cold then the tiger is nice. If someone is round and cold then they are big.
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
The tiger is red.
("tiger" "is" "red" "+")
If the tiger is red then the tiger is cold.
((("tiger" "is" "red" "+")) -> ("tiger" "is" "cold" "+"))
Cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If the tiger is cold then the tiger is big.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "big" "+"))
Round, big people are nice.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
All red, big people are cold.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
If the tiger is cold then the tiger is nice.
((("tiger" "is" "cold" "+")) -> ("tiger" "is" "nice" "+"))
If someone is round and cold then they are big.
((("someone" "is" "round" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
The tiger is nice.
True
1
proof
[(triple2 OR ((triple1) -> rule7) OR ((((triple3) -> rule1)) -> rule7))]
("tiger" "is" "nice" "+")
triple2
((triple1) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is not cold.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1) OR ((((triple2) -> rule6)) -> rule1))]
("tiger" "is" "cold" "-")
triple1
((triple3) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger does not like the tiger.
Unknown
inv-random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "-")
The tiger eats the tiger.
Unknown
random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "+")
@0: The tiger is cold.[(triple1 OR ((triple3) -> rule1) OR ((((triple2) -> rule6)) -> rule1))] The tiger is nice.[(triple2 OR ((triple1) -> rule7) OR ((((triple3) -> rule1)) -> rule7))] The tiger is red.[(triple3 OR ((triple1) -> rule2) OR ((triple2) -> rule6) OR ((((triple1) -> rule7)) -> rule6))] @1: The tiger is big.[(((triple1) -> rule3) OR ((((triple3) -> rule1)) -> rule3) OR ((((((triple2) -> rule6)) -> rule1)) -> rule3))]
The tiger is cold.
("tiger" "is" "cold" "+")
triple1
((triple3) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
((((triple2) -> (rule6 % int2))) -> (rule1 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is red.
("tiger" "is" "red" "+")
int2
The tiger is nice.
("tiger" "is" "nice" "+")
triple2
((triple1) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule7 % int1))
The tiger is nice.
("tiger" "is" "nice" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
triple3
((triple1) -> (rule2 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((triple2) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The tiger is red.
("tiger" "is" "red" "+")
int1
The tiger is nice.
("tiger" "is" "nice" "+")
int2
The tiger is big.
("tiger" "is" "big" "+")
((triple1) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
((((((triple2) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is cold.
("tiger" "is" "cold" "+")
int2
The tiger is red.
("tiger" "is" "red" "+")
int3