The squirrel is big. The squirrel is blue. The squirrel is young. Big, blue people are kind. If the squirrel is nice then the squirrel is young. If someone is big and young then they are kind. If someone is big and kind then they are blue. Big people are young. If someone is big and kind then they are young.
The squirrel is big.
("squirrel" "is" "big" "+")
The squirrel is blue.
("squirrel" "is" "blue" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
Big, blue people are kind.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
If the squirrel is nice then the squirrel is young.
((("squirrel" "is" "nice" "+")) -> ("squirrel" "is" "young" "+"))
If someone is big and young then they are kind.
((("someone" "is" "big" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
If someone is big and kind then they are blue.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
If someone is big and kind then they are young.
((("someone" "is" "big" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
The squirrel is blue.
True
1
proof
[(triple2 OR ((triple1 ((triple1 triple3) -> rule3)) -> rule4) OR ((triple1 ((triple1 ((triple1) -> rule5)) -> rule3)) -> rule4))]
("squirrel" "is" "blue" "+")
triple2
((triple1 ((triple1 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel is not young.
False
1
inv-proof
[(triple3 OR ((triple1) -> rule5) OR ((triple1 ((triple1 triple2) -> rule1)) -> rule6))]
("squirrel" "is" "young" "-")
triple3
((triple1) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1 ((triple1 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is kind.
True
3
proof
[(((triple1 triple2) -> rule1) OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple1) -> rule5)) -> rule3))]
("squirrel" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is not kind.
False
3
inv-proof
[(((triple1 triple2) -> rule1) OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple1) -> rule5)) -> rule3))]
("squirrel" "is" "kind" "-")
((triple1 triple2) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2
The squirrel is not nice.
Unknown
inv-random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
The squirrel does not like the squirrel.
Unknown
inv-random
[@0: The squirrel likes the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "likes" "squirrel" "-")
The squirrel needs the squirrel.
Unknown
random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "+")
@0: The squirrel is big.[(triple1)] The squirrel is blue.[(triple2 OR ((triple1 ((triple1 triple3) -> rule3)) -> rule4) OR ((triple1 ((triple1 ((triple1) -> rule5)) -> rule3)) -> rule4))] The squirrel is young.[(triple3 OR ((triple1) -> rule5) OR ((triple1 ((triple1 triple2) -> rule1)) -> rule6))] @1: The squirrel is kind.[(((triple1 triple2) -> rule1) OR ((triple1 triple3) -> rule3) OR ((triple1 ((triple1) -> rule5)) -> rule3))]
The squirrel is big.
("squirrel" "is" "big" "+")
triple1
The squirrel is blue.
("squirrel" "is" "blue" "+")
triple2
((triple1 ((triple1 triple3) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is young.
("squirrel" "is" "young" "+")
int3
The squirrel is young.
("squirrel" "is" "young" "+")
triple3
((triple1) -> (rule5 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
((triple1 ((triple1 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The squirrel is young.
("squirrel" "is" "young" "+")
int1
The squirrel is kind.
("squirrel" "is" "kind" "+")
int2
The squirrel is kind.
("squirrel" "is" "kind" "+")
((triple1 triple2) -> (rule1 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 triple3) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
((triple1 ((triple1) -> (rule5 % int2))) -> (rule3 % int1))
The squirrel is kind.
("squirrel" "is" "kind" "+")
int1
The squirrel is young.
("squirrel" "is" "young" "+")
int2