The squirrel is big. The squirrel is blue. The squirrel is young. If something is red then it is not blue. Big, red things are blue. If something is blue then it is kind. If something is blue and young then it is kind. All blue things are big. If something is kind then it is not red. If the squirrel is big then the squirrel is kind. If the squirrel is not young then the squirrel is not blue.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
If something is red then it is not blue.
((("something" "is" "red" "+")) -> ("something" "is" "blue" "-"))
Big, red things are blue.
((("something" "is" "big" "+") ("something" "is" "red" "+")) -> ("something" "is" "blue" "+"))
If something is blue then it is kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
If something is blue and young then it is kind.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
All blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is kind then it is not red.
((("something" "is" "kind" "+")) -> ("something" "is" "red" "-"))
If the squirrel is big then the squirrel is kind.
((("squirrel" "is" "big" "+")) -> ("squirrel" "is" "kind" "+"))
If the squirrel is not young then the squirrel is not blue.
((("squirrel" "is" "young" "~")) -> ("squirrel" "is" "blue" "-"))
The squirrel is big.
True
1
proof
[(triple1 OR ((triple2) -> rule5))]
("squirrel" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is not big.
False
1
inv-proof
[(triple1 OR ((triple2) -> rule5))]
("squirrel" "is" "big" "-")
triple1
((triple2) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is kind.
True
2
proof
[(((triple1) -> rule7) OR ((triple2) -> rule3) OR ((triple2 triple3) -> rule4) OR ((((triple2) -> rule5)) -> rule7))]
("squirrel" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2 triple3) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is not kind.
False
2
inv-proof
[(((triple1) -> rule7) OR ((triple2) -> rule3) OR ((triple2 triple3) -> rule4) OR ((((triple2) -> rule5)) -> rule7))]
("squirrel" "is" "kind" "-")
((triple1) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2 triple3) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is not red.
True
3
proof
[(((((triple1) -> rule7)) -> rule6) OR ((((triple2) -> rule3)) -> rule6) OR ((((triple2 triple3) -> rule4)) -> rule6) OR ((((((triple2) -> rule5)) -> rule7)) -> rule6))]
("squirrel" "is" "red" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
The squirrel is red.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule6) OR ((((triple2) -> rule3)) -> rule6) OR ((((triple2 triple3) -> rule4)) -> rule6) OR ((((((triple2) -> rule5)) -> rule7)) -> rule6))]
("squirrel" "is" "red" "+")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3
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 chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The squirrel is big.[(triple1 OR ((triple2) -> rule5))] The squirrel is blue.[(triple2)] The squirrel is young.[(triple3)] @1: The squirrel is kind.[(((triple1) -> rule7) OR ((triple2) -> rule3) OR ((triple2 triple3) -> rule4) OR ((((triple2) -> rule5)) -> rule7))] @2: The squirrel is not red.[(((((triple1) -> rule7)) -> rule6) OR ((((triple2) -> rule3)) -> rule6) OR ((((triple2 triple3) -> rule4)) -> rule6) OR ((((((triple2) -> rule5)) -> rule7)) -> rule6))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
((triple2) -> (rule5 % int1))
The squirrel is big.
("squirrel" "is" "big" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple2 triple3) -> (rule4 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is big.
("squirrel" "is" "big" "+")
int2
The squirrel is not red.
("squirrel" "is" "red" "-")
((((triple1) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2) -> (rule3 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((triple2 triple3) -> (rule4 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is big.
("squirrel" "is" "big" "+")
int3