The cow chases the squirrel. The dog does not see the cow. The squirrel chases the cow. If something chases the dog then the dog chases the squirrel. If something eats the dog and the dog does not eat the cow then the dog chases the squirrel. If something is red and not kind then it does not see the cow. If something eats the cow and it is not nice then the cow is green. If something chases the cow then the cow chases the dog. If something eats the squirrel and the squirrel does not eat the cow then it sees the dog.
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
The dog does not see the cow.
("dog" "sees" "cow" "-")
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
If something chases the dog then the dog chases the squirrel.
((("something" "chases" "dog" "+")) -> ("dog" "chases" "squirrel" "+"))
If something eats the dog and the dog does not eat the cow then the dog chases the squirrel.
((("something" "eats" "dog" "+") ("dog" "eats" "cow" "~")) -> ("dog" "chases" "squirrel" "+"))
If something is red and not kind then it does not see the cow.
((("something" "is" "red" "+") ("something" "is" "kind" "~")) -> ("something" "sees" "cow" "-"))
If something eats the cow and it is not nice then the cow is green.
((("something" "eats" "cow" "+") ("something" "is" "nice" "~")) -> ("cow" "is" "green" "+"))
If something chases the cow then the cow chases the dog.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "dog" "+"))
If something eats the squirrel and the squirrel does not eat the cow then it sees the dog.
((("something" "eats" "squirrel" "+") ("squirrel" "eats" "cow" "~")) -> ("something" "sees" "dog" "+"))
The dog does not see the cow.
True
1
proof
[(triple2)]
("dog" "sees" "cow" "-")
triple2
The dog sees the cow.
False
1
inv-proof
[(triple2)]
("dog" "sees" "cow" "+")
triple2
The cow chases the dog.
True
2
proof
[(((triple3) -> rule5))]
("cow" "chases" "dog" "+")
((triple3) -> (rule5 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow does not chase the dog.
False
2
inv-proof
[(((triple3) -> rule5))]
("cow" "chases" "dog" "-")
((triple3) -> (rule5 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog chases the squirrel.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("dog" "chases" "squirrel" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The dog does not chase the squirrel.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("dog" "chases" "squirrel" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The squirrel does not see the dog.
Unknown
inv-rconc
[@1: The squirrel sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "sees" "dog" "-")
The dog sees the dog.
Unknown
rconc
[@1: The dog sees the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "sees" "dog" "+")
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "green" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The cow does not eat the dog.
Unknown
inv-random
[@0: The cow eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "dog" "-")
The squirrel is kind.
Unknown
random
[@0: The squirrel is kind.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "kind" "+")
@0: The cow chases the squirrel.[(triple1)] The dog does not see the cow.[(triple2)] The squirrel chases the cow.[(triple3)] @1: The cow chases the dog.[(((triple3) -> rule5))] @2: The dog chases the squirrel.[(((((triple3) -> rule5)) -> rule1))]
The cow chases the squirrel.
("cow" "chases" "squirrel" "+")
triple1
The dog does not see the cow.
("dog" "sees" "cow" "-")
triple2
The squirrel chases the cow.
("squirrel" "chases" "cow" "+")
triple3
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple3) -> (rule5 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2