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