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