The cow needs the dog. The dog visits the rabbit. The rabbit eats the dog. If something visits the cow then the cow is red. If something is nice then it visits the cow. If something visits the dog then the dog is nice. If something visits the rabbit then it is nice. If something is nice and it eats the cow then it does not visit the rabbit. If something visits the dog then the dog does not need the cow. If something needs the cow then it is blue. If something visits the cow and the cow visits the rabbit then it is not cold.
The cow needs the dog.
("cow" "needs" "dog" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
If something visits the cow then the cow is red.
((("something" "visits" "cow" "+")) -> ("cow" "is" "red" "+"))
If something is nice then it visits the cow.
((("something" "is" "nice" "+")) -> ("something" "visits" "cow" "+"))
If something visits the dog then the dog is nice.
((("something" "visits" "dog" "+")) -> ("dog" "is" "nice" "+"))
If something visits the rabbit then it is nice.
((("something" "visits" "rabbit" "+")) -> ("something" "is" "nice" "+"))
If something is nice and it eats the cow then it does not visit the rabbit.
((("something" "is" "nice" "+") ("something" "eats" "cow" "+")) -> ("something" "visits" "rabbit" "-"))
If something visits the dog then the dog does not need the cow.
((("something" "visits" "dog" "+")) -> ("dog" "needs" "cow" "-"))
If something needs the cow then it is blue.
((("something" "needs" "cow" "+")) -> ("something" "is" "blue" "+"))
If something visits the cow and the cow visits the rabbit then it is not cold.
((("something" "visits" "cow" "+") ("cow" "visits" "rabbit" "+")) -> ("something" "is" "cold" "-"))
The cow needs the dog.
True
1
proof
[(triple1)]
("cow" "needs" "dog" "+")
triple1
The cow does not need the dog.
False
1
inv-proof
[(triple1)]
("cow" "needs" "dog" "-")
triple1
The dog is nice.
True
2
proof
[(((triple2) -> rule4))]
("dog" "is" "nice" "+")
((triple2) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog is not nice.
False
2
inv-proof
[(((triple2) -> rule4))]
("dog" "is" "nice" "-")
((triple2) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog visits the cow.
True
3
proof
[(((((triple2) -> rule4)) -> rule2))]
("dog" "visits" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The dog does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule2))]
("dog" "visits" "cow" "-")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The cow is red.
True
4
proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule1))]
("cow" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The cow is not red.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule2)) -> rule1))]
("cow" "is" "red" "-")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3
The cow does not visit the cow.
Unknown
inv-rconc
[@2: The cow visits the cow.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("cow" "visits" "cow" "-")
The rabbit is nice.
Unknown
rconc
[@1: The rabbit is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "nice" "+")
The cow is not nice.
Unknown
inv-rconc
[@1: The cow is nice.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "is" "nice" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "blue" "+")
The rabbit is not red.
Unknown
inv-random
[@0: The rabbit is red.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "red" "-")
The cow eats the rabbit.
Unknown
random
[@0: The cow eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "rabbit" "+")
The rabbit does not need the dog.
Unknown
inv-random
[@0: The rabbit needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "dog" "-")
The cow visits the rabbit.
Unknown
random
[@0: The cow visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "rabbit" "+")
@0: The cow needs the dog.[(triple1)] The dog visits the rabbit.[(triple2)] The rabbit eats the dog.[(triple3)] @1: The dog is nice.[(((triple2) -> rule4))] @2: The dog visits the cow.[(((((triple2) -> rule4)) -> rule2))] @3: The cow is red.[(((((((triple2) -> rule4)) -> rule2)) -> rule1))]
The cow needs the dog.
("cow" "needs" "dog" "+")
triple1
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple2
The rabbit eats the dog.
("rabbit" "eats" "dog" "+")
triple3
The dog is nice.
("dog" "is" "nice" "+")
((triple2) -> (rule4 % int1))
The dog is nice.
("dog" "is" "nice" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog is nice.
("dog" "is" "nice" "+")
int2
The cow is red.
("cow" "is" "red" "+")
((((((triple2) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
int2
The dog is nice.
("dog" "is" "nice" "+")
int3