The cat visits the cow. The cow needs the cat. The dog chases the cow. The squirrel chases the dog. If someone chases the dog then the dog chases the squirrel. If someone chases the squirrel then they visit the cow.
The cat visits the cow.
("cat" "visits" "cow" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
If someone chases the dog then the dog chases the squirrel.
((("someone" "chases" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If someone chases the squirrel then they visit the cow.
((("someone" "chases" "squirrel" "+")) -> ("someone" "visits" "cow" "+"))
The squirrel chases the dog.
True
1
proof
[(triple4)]
("squirrel" "chases" "dog" "+")
triple4
The cow does not need the cat.
False
1
inv-proof
[(triple2)]
("cow" "needs" "cat" "-")
triple2
The dog chases the squirrel.
True
2
proof
[(((triple4) -> rule1))]
("dog" "chases" "squirrel" "+")
((triple4) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog does not chase the squirrel.
False
2
inv-proof
[(((triple4) -> rule1))]
("dog" "chases" "squirrel" "-")
((triple4) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog visits the cow.
True
3
proof
[(((((triple4) -> rule1)) -> rule2))]
("dog" "visits" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
The dog does not visit the cow.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule2))]
("dog" "visits" "cow" "-")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2
The cow does not visit the cow.
Unknown
inv-rconc
[@1: The cow visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "visits" "cow" "-")
The squirrel visits the cow.
Unknown
rconc
[@1: The squirrel visits the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "visits" "cow" "+")
The dog is not kind.
Unknown
inv-random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "-")
The cat visits the dog.
Unknown
random
[@0: The cat visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "visits" "dog" "+")
The squirrel is not rough.
Unknown
inv-random
[@0: The squirrel is rough.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel chases the squirrel.
Unknown
random
[@0: The squirrel chases the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "squirrel" "+")
@0: The cat visits the cow.[(triple1)] The cow needs the cat.[(triple2)] The dog chases the cow.[(triple3)] The squirrel chases the dog.[(triple4)] @1: The dog chases the squirrel.[(((triple4) -> rule1))] @2: The dog visits the cow.[(((((triple4) -> rule1)) -> rule2))]
The cat visits the cow.
("cat" "visits" "cow" "+")
triple1
The cow needs the cat.
("cow" "needs" "cat" "+")
triple2
The dog chases the cow.
("dog" "chases" "cow" "+")
triple3
The squirrel chases the dog.
("squirrel" "chases" "dog" "+")
triple4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((triple4) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
((((triple4) -> (rule1 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int2