The cat is big. If the cat is red and the cat is blue then the cat is big. All cold, blue people are nice. If someone is cold and big then they are red. If someone is blue then they are nice. If the cat is nice and the cat is cold then the cat is red. Big people are cold. All red, nice people are cold. Red people are blue.
The cat is big.
("cat" "is" "big" "+")
If the cat is red and the cat is blue then the cat is big.
((("cat" "is" "red" "+") ("cat" "is" "blue" "+")) -> ("cat" "is" "big" "+"))
All cold, blue people are nice.
((("someone" "is" "cold" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If someone is cold and big then they are red.
((("someone" "is" "cold" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
If someone is blue then they are nice.
((("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "+"))
If the cat is nice and the cat is cold then the cat is red.
((("cat" "is" "nice" "+") ("cat" "is" "cold" "+")) -> ("cat" "is" "red" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
All red, nice people are cold.
((("someone" "is" "red" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
The cat is big.
True
1
proof
[(triple1)]
("cat" "is" "big" "+")
triple1
The cat is not big.
False
1
inv-proof
[(triple1)]
("cat" "is" "big" "-")
triple1
The cat is cold.
True
2
proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "is" "cold" "-")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule3))]
("cat" "is" "red" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is not red.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule3))]
("cat" "is" "red" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is blue.
True
5
proof
[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule8))]
("cat" "is" "blue" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is not blue.
False
5
inv-proof
[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule8))]
("cat" "is" "blue" "-")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is 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 sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat is big.[(triple1)] @1: The cat is cold.[(((triple1) -> rule6))] @2: The cat is red.[(((((triple1) -> rule6) triple1) -> rule3))] @3: The cat is blue.[(((((((triple1) -> rule6) triple1) -> rule3)) -> rule8))] @4: The cat is nice.[(((((((((triple1) -> rule6) triple1) -> rule3)) -> rule8)) -> rule4) OR ((((triple1) -> rule6) ((((((triple1) -> rule6) triple1) -> rule3)) -> rule8)) -> rule2))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is cold.
("cat" "is" "cold" "+")
((triple1) -> (rule6 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple1) -> (rule6 % int3)) triple1) -> (rule3 % int2))) -> (rule8 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is nice.
("cat" "is" "nice" "+")
((((((((triple1) -> (rule6 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4
((((triple1) -> (rule6 % int4)) ((((((triple1) -> (rule6 % int4)) triple1) -> (rule3 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is blue.
("cat" "is" "blue" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is cold.
("cat" "is" "cold" "+")
int4