The squirrel is big. The squirrel is green. The squirrel is kind. The squirrel is red. The squirrel is young. All kind, big people are green. All red, kind people are green. Young people are kind. Young people are kind. If the squirrel is green then the squirrel is young. All kind, red people are green. Green, big people are red. All young people are green.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is green.
("squirrel" "is" "green" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is red.
("squirrel" "is" "red" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
All kind, big people are green.
((("someone" "is" "kind" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
All red, kind people are green.
((("someone" "is" "red" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
Young people are kind.
((("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If the squirrel is green then the squirrel is young.
((("squirrel" "is" "green" "+")) -> ("squirrel" "is" "young" "+"))
All kind, red people are green.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
Green, big people are red.
((("someone" "is" "green" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "red" "+"))
All young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
The squirrel is kind.
True
1
proof
[(triple3 OR ((triple5) -> rule3) OR ((triple5) -> rule4) OR ((((triple2) -> rule5)) -> rule3) OR ((((triple2) -> rule5)) -> rule4))]
("squirrel" "is" "kind" "+")
triple3
((triple5) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple5) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is not big.
False
1
inv-proof
[(triple1)]
("squirrel" "is" "big" "-")
triple1
The squirrel does not eat the squirrel.
Unknown
inv-random
[@0: The squirrel eats the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "eats" "squirrel" "-")
The squirrel visits the squirrel.
Unknown
random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "+")
@0: The squirrel is big.[(triple1)] The squirrel is green.[(triple2 OR ((triple5) -> rule8) OR ((triple3 triple1) -> rule1) OR ((triple3 triple4) -> rule6) OR ((triple4 triple3) -> rule2) OR ((triple4 ((triple5) -> rule3)) -> rule2) OR ((triple4 ((triple5) -> rule4)) -> rule2) OR ((((triple5) -> rule3) triple1) -> rule1) OR ((((triple5) -> rule3) triple4) -> rule6) OR ((((triple5) -> rule4) triple1) -> rule1) OR ((((triple5) -> rule4) triple4) -> rule6))] The squirrel is kind.[(triple3 OR ((triple5) -> rule3) OR ((triple5) -> rule4) OR ((((triple2) -> rule5)) -> rule3) OR ((((triple2) -> rule5)) -> rule4))] The squirrel is red.[(triple4 OR ((triple2 triple1) -> rule7) OR ((((triple5) -> rule8) triple1) -> rule7) OR ((((triple3 triple1) -> rule1) triple1) -> rule7) OR ((((((triple5) -> rule3) triple1) -> rule1) triple1) -> rule7) OR ((((((triple5) -> rule4) triple1) -> rule1) triple1) -> rule7))] The squirrel is young.[(triple5 OR ((triple2) -> rule5) OR ((((triple3 triple1) -> rule1)) -> rule5) OR ((((triple3 triple4) -> rule6)) -> rule5) OR ((((triple4 triple3) -> rule2)) -> rule5))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is green.
("squirrel" "is" "green" "+")
triple2
((triple5) -> (rule8 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((triple3 triple1) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((triple3 triple4) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((triple4 triple3) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
((triple4 ((triple5) -> (rule3 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((triple4 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple5) -> (rule3 % int2)) triple1) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple5) -> (rule3 % int2)) triple4) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple5) -> (rule4 % int2)) triple1) -> (rule1 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple5) -> (rule4 % int2)) triple4) -> (rule6 % int1))
The squirrel is green.
("squirrel" "is" "green" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple3
((triple5) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple5) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
((((triple2) -> (rule5 % int2))) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is red.
("squirrel" "is" "red" "+")
triple4
((triple2 triple1) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
((((triple5) -> (rule8 % int2)) triple1) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((triple3 triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((((triple5) -> (rule3 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
((((((triple5) -> (rule4 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule7 % int1))
The squirrel is red.
("squirrel" "is" "red" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
triple5
((triple2) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((((triple3 triple1) -> (rule1 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((triple3 triple4) -> (rule6 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2
((((triple4 triple3) -> (rule2 % int2))) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is green.
("squirrel" "is" "green" "+")
int2