The cat is cold. The cat is round. The cat is young. Cold, young things are blue. If the cat is blue then the cat is big. All blue, young things are round. If something is young then it is blue. All young, round things are blue. If something is big then it is blue.
The cat is cold.
("cat" "is" "cold" "+")
The cat is round.
("cat" "is" "round" "+")
The cat is young.
("cat" "is" "young" "+")
Cold, young things are blue.
((("something" "is" "cold" "+") ("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
If the cat is blue then the cat is big.
((("cat" "is" "blue" "+")) -> ("cat" "is" "big" "+"))
All blue, young things are round.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
If something is young then it is blue.
((("something" "is" "young" "+")) -> ("something" "is" "blue" "+"))
All young, round things are blue.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
If something is big then it is blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
The cat is young.
True
1
proof
[(triple3)]
("cat" "is" "young" "+")
triple3
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cat is blue.
True
2
proof
[(((triple3) -> rule4) OR ((triple1 triple3) -> rule1) OR ((triple3 triple2) -> rule5))]
("cat" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple3 triple2) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not blue.
False
2
inv-proof
[(((triple3) -> rule4) OR ((triple1 triple3) -> rule1) OR ((triple3 triple2) -> rule5))]
("cat" "is" "blue" "-")
((triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple3 triple2) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is big.
True
3
proof
[(((((triple3) -> rule4)) -> rule2) OR ((((triple1 triple3) -> rule1)) -> rule2) OR ((((triple3 triple2) -> rule5)) -> rule2))]
("cat" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not big.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule2) OR ((((triple1 triple3) -> rule1)) -> rule2) OR ((((triple3 triple2) -> rule5)) -> rule2))]
("cat" "is" "big" "-")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cat chases the cat.
Unknown
random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "+")
@0: The cat is cold.[(triple1)] The cat is round.[(triple2 OR ((((triple3) -> rule4) triple3) -> rule3) OR ((((triple1 triple3) -> rule1) triple3) -> rule3))] The cat is young.[(triple3)] @1: The cat is blue.[(((triple3) -> rule4) OR ((triple1 triple3) -> rule1) OR ((triple3 triple2) -> rule5))] @2: The cat is big.[(((((triple3) -> rule4)) -> rule2) OR ((((triple1 triple3) -> rule1)) -> rule2) OR ((((triple3 triple2) -> rule5)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is round.
("cat" "is" "round" "+")
triple2
((((triple3) -> (rule4 % int2)) triple3) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule1 % int2)) triple3) -> (rule3 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is young.
("cat" "is" "young" "+")
triple3
The cat is blue.
("cat" "is" "blue" "+")
((triple3) -> (rule4 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple1 triple3) -> (rule1 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
((triple3 triple2) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((((triple3) -> (rule4 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple1 triple3) -> (rule1 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
((((triple3 triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2