The squirrel is rough. Nice things are rough. Rough, kind things are round. Rough things are kind. If something is nice and rough then it is big. All round, rough things are nice. If the squirrel is rough and the squirrel is kind then the squirrel is nice.
The squirrel is rough.
("squirrel" "is" "rough" "+")
Nice things are rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Rough, kind things are round.
((("something" "is" "rough" "+") ("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
If something is nice and rough then it is big.
((("something" "is" "nice" "+") ("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All round, rough things are nice.
((("something" "is" "round" "+") ("something" "is" "rough" "+")) -> ("something" "is" "nice" "+"))
If the squirrel is rough and the squirrel is kind then the squirrel is nice.
((("squirrel" "is" "rough" "+") ("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "nice" "+"))
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 kind.
True
2
proof
[(((triple1) -> rule3))]
("squirrel" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not kind.
False
2
inv-proof
[(((triple1) -> rule3))]
("squirrel" "is" "kind" "-")
((triple1) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is round.
True
4
proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("squirrel" "is" "round" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is not round.
False
4
inv-proof
[(((triple1 ((triple1) -> rule3)) -> rule2))]
("squirrel" "is" "round" "-")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
True
6
proof
[(((((triple1 ((triple1) -> rule3)) -> rule6) triple1) -> rule4) OR ((((((triple1 ((triple1) -> rule3)) -> rule2) triple1) -> rule5) triple1) -> rule4))]
("squirrel" "is" "big" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4
The squirrel is not big.
False
6
inv-proof
[(((((triple1 ((triple1) -> rule3)) -> rule6) triple1) -> rule4) OR ((((((triple1 ((triple1) -> rule3)) -> rule2) triple1) -> rule5) triple1) -> rule4))]
("squirrel" "is" "big" "-")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4
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 kind.[(((triple1) -> rule3))] @2: The squirrel is nice.[(((triple1 ((triple1) -> rule3)) -> rule6) OR ((((triple1 ((triple1) -> rule3)) -> rule2) triple1) -> rule5))] The squirrel is round.[(((triple1 ((triple1) -> rule3)) -> rule2))] @3: The squirrel is big.[(((((triple1 ((triple1) -> rule3)) -> rule6) triple1) -> rule4) OR ((((((triple1 ((triple1) -> rule3)) -> rule2) triple1) -> rule5) triple1) -> rule4))]
The squirrel is rough.
("squirrel" "is" "rough" "+")
triple1
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple1) -> (rule5 % int1))
The squirrel is nice.
("squirrel" "is" "nice" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is round.
("squirrel" "is" "round" "+")
((triple1 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
((((triple1 ((triple1) -> (rule3 % int3))) -> (rule6 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
((((((triple1 ((triple1) -> (rule3 % int4))) -> (rule2 % int3)) triple1) -> (rule5 % int2)) triple1) -> (rule4 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is nice.
("squirrel" "is" "nice" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is kind.
("squirrel" "is" "kind" "+")
int4