The squirrel is red. If someone is red then they are cold. If someone is kind and not cold then they are not blue. If the squirrel is kind and the squirrel is red then the squirrel is blue. If the squirrel is kind and the squirrel is red then the squirrel is blue. Blue people are kind. If someone is cold then they are kind. All rough people are kind. Cold people are kind.
The squirrel is red.
("squirrel" "is" "red" "+")
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
If someone is kind and not cold then they are not blue.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "blue" "-"))
If the squirrel is kind and the squirrel is red then the squirrel is blue.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "is" "blue" "+"))
If the squirrel is kind and the squirrel is red then the squirrel is blue.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "red" "+")) -> ("squirrel" "is" "blue" "+"))
Blue people are kind.
((("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If someone is cold then they are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Cold people are kind.
((("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
The squirrel is red.
True
1
proof
[(triple1)]
("squirrel" "is" "red" "+")
triple1
The squirrel is not red.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "red" "-")
triple1
The squirrel is cold.
True
2
proof
[(((triple1) -> rule1))]
("squirrel" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple1) -> rule1))]
("squirrel" "is" "cold" "-")
((triple1) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
True
3
proof
[(((((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1)) -> rule8))]
("squirrel" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is not kind.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1)) -> rule8))]
("squirrel" "is" "kind" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
True
5
proof
[(((((((triple1) -> rule1)) -> rule6) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) triple1) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule4))]
("squirrel" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel is not blue.
False
5
inv-proof
[(((((((triple1) -> rule1)) -> rule6) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) triple1) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule4))]
("squirrel" "is" "blue" "-")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The squirrel is rough.
Unknown
random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "+")
@0: The squirrel is red.[(triple1)] @1: The squirrel is cold.[(((triple1) -> rule1))] @2: The squirrel is kind.[(((((triple1) -> rule1)) -> rule6) OR ((((triple1) -> rule1)) -> rule8))] @3: The squirrel is blue.[(((((((triple1) -> rule1)) -> rule6) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule6) triple1) -> rule4) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule3) OR ((((((triple1) -> rule1)) -> rule8) triple1) -> rule4))]
The squirrel is red.
("squirrel" "is" "red" "+")
triple1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1) -> (rule1 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule1 % int3))) -> (rule8 % int2)) triple1) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3