The cat is big. All big things are red. All cold things are nice. Kind, big things are nice. Red, big things are cold. If the cat is kind and the cat is not big then the cat is cold. If the cat is kind then the cat is nice. If the cat is cold and the cat is not big then the cat is kind. All nice things are kind.
The cat is big.
("cat" "is" "big" "+")
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Kind, big things are nice.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "nice" "+"))
Red, big things are cold.
((("something" "is" "red" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If the cat is kind and the cat is not big then the cat is cold.
((("cat" "is" "kind" "+") ("cat" "is" "big" "~")) -> ("cat" "is" "cold" "+"))
If the cat is kind then the cat is nice.
((("cat" "is" "kind" "+")) -> ("cat" "is" "nice" "+"))
If the cat is cold and the cat is not big then the cat is kind.
((("cat" "is" "cold" "+") ("cat" "is" "big" "~")) -> ("cat" "is" "kind" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
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 red.
True
2
proof
[(((triple1) -> rule1))]
("cat" "is" "red" "+")
((triple1) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is not red.
False
2
inv-proof
[(((triple1) -> rule1))]
("cat" "is" "red" "-")
((triple1) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is cold.
True
4
proof
[(((((triple1) -> rule1) triple1) -> rule4))]
("cat" "is" "cold" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is not cold.
False
4
inv-proof
[(((((triple1) -> rule1) triple1) -> rule4))]
("cat" "is" "cold" "-")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "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 big.[(triple1)] @1: The cat is red.[(((triple1) -> rule1))] @2: The cat is cold.[(((((triple1) -> rule1) triple1) -> rule4))] @3: The cat is nice.[(((((((triple1) -> rule1) triple1) -> rule4)) -> rule2))] @4: The cat is kind.[(((((((((triple1) -> rule1) triple1) -> rule4)) -> rule2)) -> rule8))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat is red.
("cat" "is" "red" "+")
((triple1) -> (rule1 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat is nice.
("cat" "is" "nice" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule4 % int2))) -> (rule2 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The cat is kind.
("cat" "is" "kind" "+")
((((((((triple1) -> (rule1 % int4)) triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4