The squirrel is rough. If something is cold and blue then it is kind. All blue things are kind. Rough things are cold. Rough things are cold. If the squirrel is cold and the squirrel is rough then the squirrel is blue. If the squirrel is rough and the squirrel is not blue then the squirrel is young.
The squirrel is rough.
("squirrel" "is" "rough" "+")
If something is cold and blue then it is kind.
((("something" "is" "cold" "+") ("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
Rough things are cold.
((("something" "is" "rough" "+")) -> ("something" "is" "cold" "+"))
If the squirrel is cold and the squirrel is rough then the squirrel is blue.
((("squirrel" "is" "cold" "+") ("squirrel" "is" "rough" "+")) -> ("squirrel" "is" "blue" "+"))
If the squirrel is rough and the squirrel is not blue then the squirrel is young.
((("squirrel" "is" "rough" "+") ("squirrel" "is" "blue" "~")) -> ("squirrel" "is" "young" "+"))
The squirrel is rough.
True
1
proof
[(triple1)]
("squirrel" "is" "rough" "+")
triple1
The squirrel is not rough.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "rough" "-")
triple1
The squirrel is cold.
True
2
proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("squirrel" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is not cold.
False
2
inv-proof
[(((triple1) -> rule3) OR ((triple1) -> rule4))]
("squirrel" "is" "cold" "-")
((triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
True
4
proof
[(((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule4) triple1) -> rule5))]
("squirrel" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is not blue.
False
4
inv-proof
[(((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule4) triple1) -> rule5))]
("squirrel" "is" "blue" "-")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is kind.
True
5
proof
[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule2) OR ((((((triple1) -> rule4) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule3) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1))]
("squirrel" "is" "kind" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel is not kind.
False
5
inv-proof
[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule2) OR ((((((triple1) -> rule4) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule3) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1))]
("squirrel" "is" "kind" "-")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
The squirrel is not young.
Unknown
inv-rconc
[@1: The squirrel is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "young" "-")
The squirrel likes the squirrel.
Unknown
random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The squirrel sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The squirrel is rough.[(triple1)] @1: The squirrel is cold.[(((triple1) -> rule3) OR ((triple1) -> rule4))] @2: The squirrel is blue.[(((((triple1) -> rule3) triple1) -> rule5) OR ((((triple1) -> rule4) triple1) -> rule5))] @3: The squirrel is kind.[(((((((triple1) -> rule3) triple1) -> rule5)) -> rule2) OR ((((((triple1) -> rule4) triple1) -> rule5)) -> rule2) OR ((((triple1) -> rule3) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule3) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule3) triple1) -> rule5)) -> rule1) OR ((((triple1) -> rule4) ((((triple1) -> rule4) triple1) -> rule5)) -> rule1))]
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple1
The squirrel is cold.
("squirrel" "is" "cold" "+")
((triple1) -> (rule3 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
((triple1) -> (rule4 % int1))
The squirrel is cold.
("squirrel" "is" "cold" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((((triple1) -> (rule3 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is cold.
("squirrel" "is" "cold" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule3 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule3 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3
((((triple1) -> (rule4 % int3)) ((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
int2
The squirrel is cold.
("squirrel" "is" "cold" "+")
int3