The cow is kind. The cow is nice. The cow needs the dog. The cow visits the squirrel. The dog chases the cow. The dog is green. The dog is nice. The dog needs the cow. The dog visits the cow. The dog visits the squirrel. The squirrel chases the cow. The squirrel is kind. The squirrel is nice. The squirrel is young. The squirrel needs the dog. The squirrel visits the cow. If someone visits the cow and the cow is blue then they need the dog. If the squirrel is green then the squirrel visits the cow. If someone needs the dog then they are blue.
The cow is kind.
("cow" "is" "kind" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
The squirrel is kind.
("squirrel" "is" "kind" "+")
The squirrel is nice.
("squirrel" "is" "nice" "+")
The squirrel is young.
("squirrel" "is" "young" "+")
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
If someone visits the cow and the cow is blue then they need the dog.
((("someone" "visits" "cow" "+") ("cow" "is" "blue" "+")) -> ("someone" "needs" "dog" "+"))
If the squirrel is green then the squirrel visits the cow.
((("squirrel" "is" "green" "+")) -> ("squirrel" "visits" "cow" "+"))
If someone needs the dog then they are blue.
((("someone" "needs" "dog" "+")) -> ("someone" "is" "blue" "+"))
The squirrel is kind.
True
1
proof
[(triple12)]
("squirrel" "is" "kind" "+")
triple12
The squirrel is not young.
False
1
inv-proof
[(triple14)]
("squirrel" "is" "young" "-")
triple14
The cow is blue.
True
2
proof
[(((triple3) -> rule3))]
("cow" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The cow is not blue.
False
2
inv-proof
[(((triple3) -> rule3))]
("cow" "is" "blue" "-")
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The dog needs the dog.
True
4
proof
[(((triple9 ((triple3) -> rule3)) -> rule1))]
("dog" "needs" "dog" "+")
((triple9 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The dog does not need the dog.
False
4
inv-proof
[(((triple9 ((triple3) -> rule3)) -> rule1))]
("dog" "needs" "dog" "-")
((triple9 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The dog is blue.
True
5
proof
[(((((triple9 ((triple3) -> rule3)) -> rule1)) -> rule3))]
("dog" "is" "blue" "+")
((((triple9 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The dog is not blue.
False
5
inv-proof
[(((((triple9 ((triple3) -> rule3)) -> rule1)) -> rule3))]
("dog" "is" "blue" "-")
((((triple9 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The cow does not chase the dog.
Unknown
inv-random
[@0: The cow chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "dog" "-")
The squirrel needs the cow.
Unknown
random
[@0: The squirrel needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "cow" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
The squirrel does not need the squirrel.
Unknown
inv-random
[@0: The squirrel needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "squirrel" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
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 cow is green.
Unknown
random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "+")
@0: The cow is kind.[(triple1)] The cow is nice.[(triple2)] The cow needs the dog.[(triple3)] The cow visits the squirrel.[(triple4)] The dog chases the cow.[(triple5)] The dog is green.[(triple6)] The dog is nice.[(triple7)] The dog needs the cow.[(triple8)] The dog visits the cow.[(triple9)] The dog visits the squirrel.[(triple10)] The squirrel chases the cow.[(triple11)] The squirrel is kind.[(triple12)] The squirrel is nice.[(triple13)] The squirrel is young.[(triple14)] The squirrel needs the dog.[(triple15 OR ((triple16 ((triple3) -> rule3)) -> rule1))] The squirrel visits the cow.[(triple16)] @1: The cow is blue.[(((triple3) -> rule3))] The squirrel is blue.[(((triple15) -> rule3) OR ((((triple16 ((triple3) -> rule3)) -> rule1)) -> rule3))] @2: The dog needs the dog.[(((triple9 ((triple3) -> rule3)) -> rule1))] @3: The dog is blue.[(((((triple9 ((triple3) -> rule3)) -> rule1)) -> rule3))]
The cow is kind.
("cow" "is" "kind" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow needs the dog.
("cow" "needs" "dog" "+")
triple3
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple4
The dog chases the cow.
("dog" "chases" "cow" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog needs the cow.
("dog" "needs" "cow" "+")
triple8
The dog visits the cow.
("dog" "visits" "cow" "+")
triple9
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
triple10
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple11
The squirrel is kind.
("squirrel" "is" "kind" "+")
triple12
The squirrel is nice.
("squirrel" "is" "nice" "+")
triple13
The squirrel is young.
("squirrel" "is" "young" "+")
triple14
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
triple15
((triple16 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple16
The cow is blue.
("cow" "is" "blue" "+")
((triple3) -> (rule3 % int1))
The cow is blue.
("cow" "is" "blue" "+")
int1
The squirrel is blue.
("squirrel" "is" "blue" "+")
((triple15) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
((((triple16 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The squirrel is blue.
("squirrel" "is" "blue" "+")
int1
The squirrel needs the dog.
("squirrel" "needs" "dog" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3
The dog needs the dog.
("dog" "needs" "dog" "+")
((triple9 ((triple3) -> (rule3 % int2))) -> (rule1 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The cow is blue.
("cow" "is" "blue" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((triple9 ((triple3) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The dog needs the dog.
("dog" "needs" "dog" "+")
int2
The cow is blue.
("cow" "is" "blue" "+")
int3