The squirrel is big. The squirrel is kind. The squirrel is not red. The squirrel is round. The squirrel is not young. All big things are not young. All red things are young. If something is red then it is young. If something is red and not round then it is not young. Big things are kind. If something is kind and not round then it is not big. If the squirrel is kind and the squirrel is not big then the squirrel is young. If the squirrel is kind then the squirrel is not young.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is not red.
("squirrel" "is" "red" "-")
The squirrel is round.
("squirrel" "is" "round" "+")
The squirrel is not young.
("squirrel" "is" "young" "-")
All big things are not young.
((("something" "is" "big" "+")) -> ("something" "is" "young" "-"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is red then it is young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is red and not round then it is not young.
((("something" "is" "red" "+") ("something" "is" "round" "~")) -> ("something" "is" "young" "-"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
If something is kind and not round then it is not big.
((("something" "is" "kind" "+") ("something" "is" "round" "~")) -> ("something" "is" "big" "-"))
If the squirrel is kind and the squirrel is not big then the squirrel is young.
((("squirrel" "is" "kind" "+") ("squirrel" "is" "big" "~")) -> ("squirrel" "is" "young" "+"))
If the squirrel is kind then the squirrel is not young.
((("squirrel" "is" "kind" "+")) -> ("squirrel" "is" "young" "-"))
The squirrel is not young.
True
1
proof
[(triple5 OR ((triple1) -> rule1) OR ((triple2) -> rule8) OR ((((triple1) -> rule5)) -> rule8))]
("squirrel" "is" "young" "-")
triple5
((triple1) -> (rule1 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((triple2) -> (rule8 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is red.
False
1
inv-proof
[(triple3)]
("squirrel" "is" "red" "+")
triple3
The squirrel does not see the squirrel.
Unknown
inv-random
[@0: The squirrel sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "sees" "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 kind.[(triple2 OR ((triple1) -> rule5))] The squirrel is not red.[(triple3)] The squirrel is not young.[(triple5 OR ((triple1) -> rule1) OR ((triple2) -> rule8) OR ((((triple1) -> rule5)) -> rule8))] The squirrel is round.[(triple4)]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple2
((triple1) -> (rule5 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is not red.
("squirrel" "is" "red" "-")
triple3
The squirrel is not young.
("squirrel" "is" "young" "-")
triple5
((triple1) -> (rule1 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((triple2) -> (rule8 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
((((triple1) -> (rule5 % int2))) -> (rule8 % int1))
The squirrel is not young.
("squirrel" "is" "young" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is round.
("squirrel" "is" "round" "+")
triple4