The squirrel is young. If something is red then it is young. All young, round things are green. If something is nice then it is not green. Young things are round. Nice things are round. Nice things are red. If the squirrel is green then the squirrel is not nice. If the squirrel is young and the squirrel is nice then the squirrel is round.
The squirrel is young.
("squirrel" "is" "young" "+")
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
All young, round things are green.
((("something" "is" "young" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
If something is nice then it is not green.
((("something" "is" "nice" "+")) -> ("something" "is" "green" "-"))
Young things are round.
((("something" "is" "young" "+")) -> ("something" "is" "round" "+"))
Nice things are round.
((("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
Nice things are red.
((("something" "is" "nice" "+")) -> ("something" "is" "red" "+"))
If the squirrel is green then the squirrel is not nice.
((("squirrel" "is" "green" "+")) -> ("squirrel" "is" "nice" "-"))
If the squirrel is young and the squirrel is nice then the squirrel is round.
((("squirrel" "is" "young" "+") ("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "round" "+"))
The squirrel is young.
True
1
proof
[(triple1)]
("squirrel" "is" "young" "+")
triple1
The squirrel is not young.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "young" "-")
triple1
The squirrel is round.
True
2
proof
[(((triple1) -> rule4))]
("squirrel" "is" "round" "+")
((triple1) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is not round.
False
2
inv-proof
[(((triple1) -> rule4))]
("squirrel" "is" "round" "-")
((triple1) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is green.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("squirrel" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not green.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule2))]
("squirrel" "is" "green" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not nice.
True
5
proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule7))]
("squirrel" "is" "nice" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is nice.
False
5
inv-proof
[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule7))]
("squirrel" "is" "nice" "+")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3
The squirrel is not red.
Unknown
inv-rconc
[@1: The squirrel is red.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "is" "red" "-")
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 sees the squirrel.
Unknown
random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "squirrel" "+")
@0: The squirrel is young.[(triple1)] @1: The squirrel is round.[(((triple1) -> rule4))] @2: The squirrel is green.[(((triple1 ((triple1) -> rule4)) -> rule2))] @3: The squirrel is not nice.[(((((triple1 ((triple1) -> rule4)) -> rule2)) -> rule7))]
The squirrel is young.
("squirrel" "is" "young" "+")
triple1
The squirrel is round.
("squirrel" "is" "round" "+")
((triple1) -> (rule4 % int1))
The squirrel is round.
("squirrel" "is" "round" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is round.
("squirrel" "is" "round" "+")
int2
The squirrel is not nice.
("squirrel" "is" "nice" "-")
((((triple1 ((triple1) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
The squirrel is not nice.
("squirrel" "is" "nice" "-")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
int3