The cat is round. If the cat is round and the cat is young then the cat is blue. If something is red then it is big. If the cat is round and the cat is red then the cat is blue. If something is blue then it is young. If something is young then it is big. All red things are round. All young, round things are big. Round things are red.
The cat is round.
("cat" "is" "round" "+")
If the cat is round and the cat is young then the cat is blue.
((("cat" "is" "round" "+") ("cat" "is" "young" "+")) -> ("cat" "is" "blue" "+"))
If something is red then it is big.
((("something" "is" "red" "+")) -> ("something" "is" "big" "+"))
If the cat is round and the cat is red then the cat is blue.
((("cat" "is" "round" "+") ("cat" "is" "red" "+")) -> ("cat" "is" "blue" "+"))
If something is blue then it is young.
((("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
All red things are round.
((("something" "is" "red" "+")) -> ("something" "is" "round" "+"))
All young, round things are big.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
The cat is round.
True
1
proof
[(triple1)]
("cat" "is" "round" "+")
triple1
The cat is not round.
False
1
inv-proof
[(triple1)]
("cat" "is" "round" "-")
triple1
The cat is red.
True
2
proof
[(((triple1) -> rule8))]
("cat" "is" "red" "+")
((triple1) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule8))]
("cat" "is" "red" "-")
((triple1) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is blue.
True
4
proof
[(((triple1 ((triple1) -> rule8)) -> rule3))]
("cat" "is" "blue" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule8)) -> rule3))]
("cat" "is" "blue" "-")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
True
5
proof
[(((((triple1 ((triple1) -> rule8)) -> rule3)) -> rule4))]
("cat" "is" "young" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is not young.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule8)) -> rule3)) -> rule4))]
("cat" "is" "young" "-")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat does not like the cat.
Unknown
inv-random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "-")
The cat visits the cat.
Unknown
random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "+")
@0: The cat is round.[(triple1)] @1: The cat is red.[(((triple1) -> rule8))] @2: The cat is big.[(((((triple1) -> rule8)) -> rule2) OR ((((((triple1 ((triple1) -> rule8)) -> rule3)) -> rule4)) -> rule5) OR ((((((triple1 ((triple1) -> rule8)) -> rule3)) -> rule4) triple1) -> rule7))] The cat is blue.[(((triple1 ((triple1) -> rule8)) -> rule3))] @3: The cat is young.[(((((triple1 ((triple1) -> rule8)) -> rule3)) -> rule4))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule8 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is big.
("cat" "is" "big" "+")
((((triple1) -> (rule8 % int2))) -> (rule2 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
((((((triple1 ((triple1) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2)) triple1) -> (rule7 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The cat is young.
("cat" "is" "young" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The cat is blue.
("cat" "is" "blue" "+")
((triple1 ((triple1) -> (rule8 % int2))) -> (rule3 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is young.
("cat" "is" "young" "+")
((((triple1 ((triple1) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The cat is young.
("cat" "is" "young" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3