The cow is big. The cow is red. The cow needs the dog. The cow visits the rabbit. The dog needs the cow. The dog visits the cow. The rabbit needs the cow. If something needs the rabbit then the rabbit likes the dog. If something needs the rabbit then it visits the cow. If something visits the rabbit and it likes the cow then the rabbit needs the dog. If something likes the dog and it needs the cow then the dog needs the rabbit. If something is red then it needs the rabbit. If something likes the dog and the dog likes the rabbit then the dog likes the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is red.
("cow" "is" "red" "+")
The cow needs the dog.
("cow" "needs" "dog" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
If something needs the rabbit then the rabbit likes the dog.
((("something" "needs" "rabbit" "+")) -> ("rabbit" "likes" "dog" "+"))
If something needs the rabbit then it visits the cow.
((("something" "needs" "rabbit" "+")) -> ("something" "visits" "cow" "+"))
If something visits the rabbit and it likes the cow then the rabbit needs the dog.
((("something" "visits" "rabbit" "+") ("something" "likes" "cow" "+")) -> ("rabbit" "needs" "dog" "+"))
If something likes the dog and it needs the cow then the dog needs the rabbit.
((("something" "likes" "dog" "+") ("something" "needs" "cow" "+")) -> ("dog" "needs" "rabbit" "+"))
If something is red then it needs the rabbit.
((("something" "is" "red" "+")) -> ("something" "needs" "rabbit" "+"))
If something likes the dog and the dog likes the rabbit then the dog likes the cow.
((("something" "likes" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("dog" "likes" "cow" "+"))
The cow is red.
True
1
proof
[(triple2)]
("cow" "is" "red" "+")
triple2
The cow does not visit the rabbit.
False
1
inv-proof
[(triple4)]
("cow" "visits" "rabbit" "-")
triple4
The cow needs the rabbit.
True
2
proof
[(((triple2) -> rule5))]
("cow" "needs" "rabbit" "+")
((triple2) -> (rule5 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow does not need the rabbit.
False
2
inv-proof
[(((triple2) -> rule5))]
("cow" "needs" "rabbit" "-")
((triple2) -> (rule5 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow visits the cow.
True
3
proof
[(((((triple2) -> rule5)) -> rule2))]
("cow" "visits" "cow" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit does not like the dog.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("rabbit" "likes" "dog" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The dog needs the rabbit.
True
5
proof
[(((((((triple2) -> rule5)) -> rule1) triple7) -> rule4))]
("dog" "needs" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The dog does not need the rabbit.
False
5
inv-proof
[(((((((triple2) -> rule5)) -> rule1) triple7) -> rule4))]
("dog" "needs" "rabbit" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The rabbit does not need the dog.
Unknown
inv-rconc
[@1: The rabbit needs the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "needs" "dog" "-")
The rabbit needs the rabbit.
Unknown
rconc
[@1: The rabbit needs the rabbit.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "needs" "rabbit" "+")
The dog does not like the cow.
Unknown
inv-rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "likes" "cow" "-")
The rabbit visits the cow.
Unknown
rconc
[@2: The rabbit visits the cow.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("rabbit" "visits" "cow" "+")
The cow is not green.
Unknown
inv-random
[@0: The cow is green.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "green" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The dog is not young.
Unknown
inv-random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "-")
The rabbit visits the dog.
Unknown
random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "+")
@0: The cow is big.[(triple1)] The cow is red.[(triple2)] The cow needs the dog.[(triple3)] The cow visits the rabbit.[(triple4)] The dog needs the cow.[(triple5)] The dog visits the cow.[(triple6 OR ((((((((triple2) -> rule5)) -> rule1) triple7) -> rule4)) -> rule2))] The rabbit needs the cow.[(triple7)] @1: The cow needs the rabbit.[(((triple2) -> rule5))] @2: The cow visits the cow.[(((((triple2) -> rule5)) -> rule2))] The rabbit likes the dog.[(((((triple2) -> rule5)) -> rule1))] @3: The dog needs the rabbit.[(((((((triple2) -> rule5)) -> rule1) triple7) -> rule4))]
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is red.
("cow" "is" "red" "+")
triple2
The cow needs the dog.
("cow" "needs" "dog" "+")
triple3
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple4
The dog needs the cow.
("dog" "needs" "cow" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
((((((((triple2) -> (rule5 % int4))) -> (rule1 % int3)) triple7) -> (rule4 % int2))) -> (rule2 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int4
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple7
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((triple2) -> (rule5 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple2) -> (rule5 % int2))) -> (rule2 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2)) triple7) -> (rule4 % int1))
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
int1
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3