The cat is cold. If something is cold then it is kind. Nice, kind things are blue. Cold things are kind. All kind, cold things are nice. Cold, blue things are kind. If something is cold and kind then it is red.
The cat is cold.
("cat" "is" "cold" "+")
If something is cold then it is kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Nice, kind things are blue.
((("something" "is" "nice" "+") ("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
All kind, cold things are nice.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Cold, blue things are kind.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is cold and kind then it is red.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "red" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cat is not cold.
False
1
inv-proof
[(triple1)]
("cat" "is" "cold" "-")
triple1
The cat is kind.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("cat" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is not kind.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule3))]
("cat" "is" "kind" "-")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
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 needs the cat.
Unknown
random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "+")
@0: The cat is cold.[(triple1)] @1: The cat is kind.[(((triple1) -> rule1) OR ((triple1) -> rule3))] @2: The cat is nice.[(((((triple1) -> rule1) triple1) -> rule4) OR ((((triple1) -> rule3) triple1) -> rule4))] The cat is red.[(((triple1 ((triple1) -> rule1)) -> rule6) OR ((triple1 ((triple1) -> rule3)) -> rule6))] @3: The cat is blue.[(((((((triple1) -> rule1) triple1) -> rule4) ((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule1) triple1) -> rule4) ((triple1) -> rule3)) -> rule2) OR ((((((triple1) -> rule3) triple1) -> rule4) ((triple1) -> rule1)) -> rule2) OR ((((((triple1) -> rule3) triple1) -> rule4) ((triple1) -> rule3)) -> rule2))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat is kind.
("cat" "is" "kind" "+")
((triple1) -> (rule1 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
((triple1) -> (rule3 % int1))
The cat is kind.
("cat" "is" "kind" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
((((triple1) -> (rule1 % int2)) triple1) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((((triple1) -> (rule3 % int2)) triple1) -> (rule4 % int1))
The cat is nice.
("cat" "is" "nice" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is red.
("cat" "is" "red" "+")
((triple1 ((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat is kind.
("cat" "is" "kind" "+")
int2
The cat is blue.
("cat" "is" "blue" "+")
((((((triple1) -> (rule1 % int3)) triple1) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((((((triple1) -> (rule1 % int3)) triple1) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule4 % int2)) ((triple1) -> (rule1 % int3))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3
((((((triple1) -> (rule3 % int3)) triple1) -> (rule4 % int2)) ((triple1) -> (rule3 % int3))) -> (rule2 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cat is nice.
("cat" "is" "nice" "+")
int2
The cat is kind.
("cat" "is" "kind" "+")
int3