The tiger is big. The tiger is blue. The tiger is nice. Nice things are big. If something is kind and not nice then it is not big. If something is big then it is not kind. If the tiger is not big then the tiger is blue. If the tiger is not kind then the tiger is cold. If the tiger is not nice and the tiger is not big then the tiger is cold. Kind, blue things are not cold. If something is blue and not kind then it is cold.
The tiger is big.
("tiger" "is" "big" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is nice.
("tiger" "is" "nice" "+")
Nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
If something is kind and not nice then it is not big.
((("something" "is" "kind" "+") ("something" "is" "nice" "~")) -> ("something" "is" "big" "-"))
If something is big then it is not kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "-"))
If the tiger is not big then the tiger is blue.
((("tiger" "is" "big" "~")) -> ("tiger" "is" "blue" "+"))
If the tiger is not kind then the tiger is cold.
((("tiger" "is" "kind" "~")) -> ("tiger" "is" "cold" "+"))
If the tiger is not nice and the tiger is not big then the tiger is cold.
((("tiger" "is" "nice" "~") ("tiger" "is" "big" "~")) -> ("tiger" "is" "cold" "+"))
Kind, blue things are not cold.
((("something" "is" "kind" "+") ("something" "is" "blue" "+")) -> ("something" "is" "cold" "-"))
If something is blue and not kind then it is cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "~")) -> ("something" "is" "cold" "+"))
The tiger is big.
True
1
proof
[(triple1 OR ((triple3) -> rule1))]
("tiger" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not big.
False
1
inv-proof
[(triple1 OR ((triple3) -> rule1))]
("tiger" "is" "big" "-")
triple1
((triple3) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is not kind.
True
2
proof
[(((triple1) -> rule3) OR ((((triple3) -> rule1)) -> rule3))]
("tiger" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is kind.
False
2
inv-proof
[(((triple1) -> rule3) OR ((((triple3) -> rule1)) -> rule3))]
("tiger" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule5) OR ((triple2 ((triple1) -> rule3)) -> rule8) OR ((((((triple3) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple3) -> rule1)) -> rule3)) -> rule8))]
("tiger" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple2 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
The tiger is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule5) OR ((triple2 ((triple1) -> rule3)) -> rule8) OR ((((((triple3) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple3) -> rule1)) -> rule3)) -> rule8))]
("tiger" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple2 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
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 ((triple3) -> rule1))] The tiger is blue.[(triple2)] The tiger is nice.[(triple3)] @1: The tiger is not kind.[(((triple1) -> rule3) OR ((((triple3) -> rule1)) -> rule3))] @2: The tiger is cold.[(((((triple1) -> rule3)) -> rule5) OR ((triple2 ((triple1) -> rule3)) -> rule8) OR ((((((triple3) -> rule1)) -> rule3)) -> rule5) OR ((triple2 ((((triple3) -> rule1)) -> rule3)) -> rule8))]
The tiger is big.
("tiger" "is" "big" "+")
triple1
((triple3) -> (rule1 % int1))
The tiger is big.
("tiger" "is" "big" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
triple2
The tiger is nice.
("tiger" "is" "nice" "+")
triple3
The tiger is not kind.
("tiger" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
((((triple3) -> (rule1 % int2))) -> (rule3 % int1))
The tiger is not kind.
("tiger" "is" "kind" "-")
int1
The tiger is big.
("tiger" "is" "big" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((triple2 ((triple1) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
((((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule5 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3
((triple2 ((((triple3) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule8 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger is not kind.
("tiger" "is" "kind" "-")
int2
The tiger is big.
("tiger" "is" "big" "+")
int3