The cat is nice. The cat visits the cow. The cat visits the squirrel. The cow does not visit the cat. The dog chases the squirrel. The dog is green. The squirrel is not green. If someone chases the squirrel then the squirrel does not need the cat. If someone chases the dog then they are green. If someone chases the squirrel then the squirrel is not red. If someone visits the cow and they are not green then the cow visits the squirrel. If the squirrel needs the dog and the dog visits the squirrel then the squirrel is not nice. If someone is red and they do not need the squirrel then the squirrel chases the cat. If someone visits the squirrel then they are red. If someone visits the dog then the dog visits the squirrel. If someone is red then they visit the dog.
The cat is nice.
("cat" "is" "nice" "+")
The cat visits the cow.
("cat" "visits" "cow" "+")
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
The cow does not visit the cat.
("cow" "visits" "cat" "-")
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
The dog is green.
("dog" "is" "green" "+")
The squirrel is not green.
("squirrel" "is" "green" "-")
If someone chases the squirrel then the squirrel does not need the cat.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "needs" "cat" "-"))
If someone chases the dog then they are green.
((("someone" "chases" "dog" "+")) -> ("someone" "is" "green" "+"))
If someone chases the squirrel then the squirrel is not red.
((("someone" "chases" "squirrel" "+")) -> ("squirrel" "is" "red" "-"))
If someone visits the cow and they are not green then the cow visits the squirrel.
((("someone" "visits" "cow" "+") ("someone" "is" "green" "~")) -> ("cow" "visits" "squirrel" "+"))
If the squirrel needs the dog and the dog visits the squirrel then the squirrel is not nice.
((("squirrel" "needs" "dog" "+") ("dog" "visits" "squirrel" "+")) -> ("squirrel" "is" "nice" "-"))
If someone is red and they do not need the squirrel then the squirrel chases the cat.
((("someone" "is" "red" "+") ("someone" "needs" "squirrel" "~")) -> ("squirrel" "chases" "cat" "+"))
If someone visits the squirrel then they are red.
((("someone" "visits" "squirrel" "+")) -> ("someone" "is" "red" "+"))
If someone visits the dog then the dog visits the squirrel.
((("someone" "visits" "dog" "+")) -> ("dog" "visits" "squirrel" "+"))
If someone is red then they visit the dog.
((("someone" "is" "red" "+")) -> ("someone" "visits" "dog" "+"))
The cat visits the cow.
True
1
proof
[(triple2)]
("cat" "visits" "cow" "+")
triple2
The squirrel is green.
False
1
inv-proof
[(triple7)]
("squirrel" "is" "green" "+")
triple7
The squirrel does not need the cat.
True
2
proof
[(((triple5) -> rule1))]
("squirrel" "needs" "cat" "-")
((triple5) -> (rule1 % int1))
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
int1
The cat is not red.
False
2
inv-proof
[(((triple3) -> rule7))]
("cat" "is" "red" "-")
((triple3) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The cat visits the dog.
True
3
proof
[(((((triple3) -> rule7)) -> rule9))]
("cat" "visits" "dog" "+")
((((triple3) -> (rule7 % int2))) -> (rule9 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The cat does not visit the dog.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule9))]
("cat" "visits" "dog" "-")
((((triple3) -> (rule7 % int2))) -> (rule9 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog visits the squirrel.
True
4
proof
[(((((((triple3) -> rule7)) -> rule9)) -> rule8))]
("dog" "visits" "squirrel" "+")
((((((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog does not visit the squirrel.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule9)) -> rule8))]
("dog" "visits" "squirrel" "-")
((((((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog is red.
True
5
proof
[(((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7))]
("dog" "is" "red" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The dog is not red.
False
5
inv-proof
[(((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7))]
("dog" "is" "red" "-")
((((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The dog visits the dog.
True
6
proof
[(((((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7)) -> rule9))]
("dog" "visits" "dog" "+")
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5
The dog does not visit the dog.
False
6
inv-proof
[(((((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7)) -> rule9))]
("dog" "visits" "dog" "-")
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5
The cow is not red.
Unknown
inv-rconc
[@2: The cow is red.[CWA. Example of deepest failure = (rule7 <- rule4 <- FAIL)]]
("cow" "is" "red" "-")
The cow visits the squirrel.
Unknown
rconc
[@1: The cow visits the squirrel.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "visits" "squirrel" "+")
The squirrel does not visit the dog.
Unknown
inv-rconc
[@1: The squirrel visits the dog.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("squirrel" "visits" "dog" "-")
The cat is green.
Unknown
rconc
[@1: The cat is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "is" "green" "+")
The cow is not green.
Unknown
inv-rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "green" "-")
The squirrel chases the cat.
Unknown
rconc
[@1: The squirrel chases the cat.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("squirrel" "chases" "cat" "+")
The cow does not need the cat.
Unknown
inv-random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "-")
The squirrel is nice.
Unknown
random
[@0: The squirrel is nice.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "is" "nice" "+")
The squirrel does not need the dog.
Unknown
inv-random
[@0: The squirrel needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "needs" "dog" "-")
The cow needs the squirrel.
Unknown
random
[@0: The cow needs the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "squirrel" "+")
The cat does not chase the cow.
Unknown
inv-random
[@0: The cat chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cow" "-")
The dog needs the cat.
Unknown
random
[@0: The dog needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cat" "+")
@0: The cat is nice.[(triple1)] The cat visits the cow.[(triple2)] The cat visits the squirrel.[(triple3)] The cow does not visit the cat.[(triple4)] The dog chases the squirrel.[(triple5)] The dog is green.[(triple6)] The squirrel is not green.[(triple7)] @1: The cat is red.[(((triple3) -> rule7))] The squirrel does not need the cat.[(((triple5) -> rule1))] The squirrel is not red.[(((triple5) -> rule3))] @2: The cat visits the dog.[(((((triple3) -> rule7)) -> rule9))] @3: The dog visits the squirrel.[(((((((triple3) -> rule7)) -> rule9)) -> rule8))] @4: The dog is red.[(((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7))] @5: The dog visits the dog.[(((((((((((triple3) -> rule7)) -> rule9)) -> rule8)) -> rule7)) -> rule9))]
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cat visits the cow.
("cat" "visits" "cow" "+")
triple2
The cat visits the squirrel.
("cat" "visits" "squirrel" "+")
triple3
The cow does not visit the cat.
("cow" "visits" "cat" "-")
triple4
The dog chases the squirrel.
("dog" "chases" "squirrel" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The squirrel is not green.
("squirrel" "is" "green" "-")
triple7
The cat is red.
("cat" "is" "red" "+")
((triple3) -> (rule7 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
((triple5) -> (rule1 % int1))
The squirrel does not need the cat.
("squirrel" "needs" "cat" "-")
int1
The squirrel is not red.
("squirrel" "is" "red" "-")
((triple5) -> (rule3 % int1))
The squirrel is not red.
("squirrel" "is" "red" "-")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
((((triple3) -> (rule7 % int2))) -> (rule9 % int1))
The cat visits the dog.
("cat" "visits" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
((((((triple3) -> (rule7 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The dog is red.
("dog" "is" "red" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule9 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
The dog is red.
("dog" "is" "red" "+")
int1
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int2
The cat visits the dog.
("cat" "visits" "dog" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The dog visits the dog.
("dog" "visits" "dog" "+")
((((((((((triple3) -> (rule7 % int5))) -> (rule9 % int4))) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule9 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The dog is red.
("dog" "is" "red" "+")
int2
The dog visits the squirrel.
("dog" "visits" "squirrel" "+")
int3
The cat visits the dog.
("cat" "visits" "dog" "+")
int4
The cat is red.
("cat" "is" "red" "+")
int5