The cow chases the dog. The cow is green. The cow is kind. The cow needs the squirrel. The dog chases the squirrel. The dog is red. The dog is round. The dog visits the cow. The squirrel chases the dog. The squirrel is not round. The squirrel needs the cow. The squirrel visits the dog. If someone is kind then they visit the dog. If someone visits the cow then the cow chases the dog. If someone is green and they chase the dog then the dog is kind. If someone is round and they do not chase the squirrel then the squirrel needs the dog. If someone needs the cow and they visit the dog then the dog chases the cow. If someone visits the squirrel and the squirrel visits the dog then the squirrel does not chase the cow.
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
The squirrel is not round.
("squirrel" "is" "round" "-")
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
If someone is kind then they visit the dog.
((("someone" "is" "kind" "+")) -> ("someone" "visits" "dog" "+"))
If someone visits the cow then the cow chases the dog.
((("someone" "visits" "cow" "+")) -> ("cow" "chases" "dog" "+"))
If someone is green and they chase the dog then the dog is kind.
((("someone" "is" "green" "+") ("someone" "chases" "dog" "+")) -> ("dog" "is" "kind" "+"))
If someone is round and they do not chase the squirrel then the squirrel needs the dog.
((("someone" "is" "round" "+") ("someone" "chases" "squirrel" "~")) -> ("squirrel" "needs" "dog" "+"))
If someone needs the cow and they visit the dog then the dog chases the cow.
((("someone" "needs" "cow" "+") ("someone" "visits" "dog" "+")) -> ("dog" "chases" "cow" "+"))
If someone visits the squirrel and the squirrel visits the dog then the squirrel does not chase the cow.
((("someone" "visits" "squirrel" "+") ("squirrel" "visits" "dog" "+")) -> ("squirrel" "chases" "cow" "-"))
The squirrel is not round.
True
1
proof
[(triple10)]
("squirrel" "is" "round" "-")
triple10
The cow does not chase the dog.
False
1
inv-proof
[(triple1 OR ((triple8) -> rule2))]
("cow" "chases" "dog" "-")
triple1
((triple8) -> (rule2 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog chases the cow.
True
3
proof
[(((triple11 triple12) -> rule5))]
("dog" "chases" "cow" "+")
((triple11 triple12) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is not kind.
False
3
inv-proof
[(((triple2 triple1) -> rule3) OR ((triple2 ((triple8) -> rule2)) -> rule3))]
("dog" "is" "kind" "-")
((triple2 triple1) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((triple2 ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog visits the dog.
True
4
proof
[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 ((triple8) -> rule2)) -> rule3)) -> rule1))]
("dog" "visits" "dog" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
((((triple2 ((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The dog does not visit the dog.
False
4
inv-proof
[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 ((triple8) -> rule2)) -> rule3)) -> rule1))]
("dog" "visits" "dog" "-")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
((((triple2 ((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3
The squirrel does not need the dog.
Unknown
inv-rconc
[@1: The squirrel needs the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "needs" "dog" "-")
The squirrel visits the cow.
Unknown
random
[@0: The squirrel visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "cow" "+")
The squirrel is not green.
Unknown
inv-random
[@0: The squirrel is green.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "green" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The cow is not round.
Unknown
inv-random
[@0: The cow is round.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "round" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
@0: The cow chases the dog.[(triple1 OR ((triple8) -> rule2))] The cow is green.[(triple2)] The cow is kind.[(triple3)] The cow needs the squirrel.[(triple4)] The dog chases the squirrel.[(triple5)] The dog is red.[(triple6)] The dog is round.[(triple7)] The dog visits the cow.[(triple8)] The squirrel chases the dog.[(triple9)] The squirrel is not round.[(triple10)] The squirrel needs the cow.[(triple11)] The squirrel visits the dog.[(triple12)] @1: The cow visits the dog.[(((triple3) -> rule1))] The dog chases the cow.[(((triple11 triple12) -> rule5))] The dog is kind.[(((triple2 triple1) -> rule3) OR ((triple2 ((triple8) -> rule2)) -> rule3))] @2: The dog visits the dog.[(((((triple2 triple1) -> rule3)) -> rule1) OR ((((triple2 ((triple8) -> rule2)) -> rule3)) -> rule1))]
The cow chases the dog.
("cow" "chases" "dog" "+")
triple1
((triple8) -> (rule2 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
triple2
The cow is kind.
("cow" "is" "kind" "+")
triple3
The cow needs the squirrel.
("cow" "needs" "squirrel" "+")
triple4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple5
The dog is red.
("dog" "is" "red" "+")
triple6
The dog is round.
("dog" "is" "round" "+")
triple7
The dog visits the cow.
("dog" "visits" "cow" "+")
triple8
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple9
The squirrel is not round.
("squirrel" "is" "round" "-")
triple10
The squirrel needs the cow.
("squirrel" "needs" "cow" "+")
triple11
The squirrel visits the dog.
("squirrel" "visits" "dog" "+")
triple12
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple3) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The dog chases the cow.
("dog" "chases" "cow" "+")
((triple11 triple12) -> (rule5 % int1))
The dog chases the cow.
("dog" "chases" "cow" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
((triple2 triple1) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
((triple2 ((triple8) -> (rule2 % int2))) -> (rule3 % int1))
The dog is kind.
("dog" "is" "kind" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog visits the dog.
("dog" "visits" "dog" "+")
((((triple2 triple1) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
((((triple2 ((triple8) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is kind.
("dog" "is" "kind" "+")
int2
The cow chases the dog.
("cow" "chases" "dog" "+")
int3