The cat is young. If something is red and not young then it is not cold. All young things are not cold. If something is blue then it is green. Green things are blue. If something is red then it is not blue. If something is young and not cold then it is blue.
The cat is young.
("cat" "is" "young" "+")
If something is red and not young then it is not cold.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "cold" "-"))
All young things are not cold.
((("something" "is" "young" "+")) -> ("something" "is" "cold" "-"))
If something is blue then it is green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
If something is red then it is not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
If something is young and not cold then it is blue.
((("something" "is" "young" "+") ("something" "is" "cold" "~")) -> ("something" "is" "blue" "+"))
The cat is young.
True
1
proof
[(triple1)]
("cat" "is" "young" "+")
triple1
The cat is not young.
False
1
inv-proof
[(triple1)]
("cat" "is" "young" "-")
triple1
The cat is not cold.
True
2
proof
[(((triple1) -> rule2))]
("cat" "is" "cold" "-")
((triple1) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat is cold.
False
2
inv-proof
[(((triple1) -> rule2))]
("cat" "is" "cold" "+")
((triple1) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat is blue.
True
4
proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("cat" "is" "blue" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not cold.
("cat" "is" "cold" "-")
int2
The cat is not blue.
False
4
inv-proof
[(((triple1 ((triple1) -> rule2)) -> rule6))]
("cat" "is" "blue" "-")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not cold.
("cat" "is" "cold" "-")
int2
The cat is green.
True
5
proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule3))]
("cat" "is" "green" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not cold.
("cat" "is" "cold" "-")
int3
The cat is not green.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule3))]
("cat" "is" "green" "-")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not cold.
("cat" "is" "cold" "-")
int3
The cat does not visit the cat.
Unknown
inv-random
[@0: The cat visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "cat" "-")
The cat likes the cat.
Unknown
random
[@0: The cat likes the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "likes" "cat" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The cat needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is young.[(triple1)] @1: The cat is not cold.[(((triple1) -> rule2))] @2: The cat is blue.[(((triple1 ((triple1) -> rule2)) -> rule6))] @3: The cat is green.[(((((triple1 ((triple1) -> rule2)) -> rule6)) -> rule3))]
The cat is young.
("cat" "is" "young" "+")
triple1
The cat is not cold.
("cat" "is" "cold" "-")
((triple1) -> (rule2 % int1))
The cat is not cold.
("cat" "is" "cold" "-")
int1
The cat is blue.
("cat" "is" "blue" "+")
((triple1 ((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is not cold.
("cat" "is" "cold" "-")
int2
The cat is green.
("cat" "is" "green" "+")
((((triple1 ((triple1) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The cat is green.
("cat" "is" "green" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is not cold.
("cat" "is" "cold" "-")
int3