The cow is big. The cow is nice. The cow is round. The cow sees the dog. The cow does not visit the dog. The dog is round. The dog does not see the cow. If something is red then it does not need the dog. If something sees the dog then it needs the dog. If the cow needs the dog then the dog visits the cow. If something sees the dog and it needs the cow then it is not kind. If something is big and it does not need the dog then it does not need the cow. If something visits the dog then it does not need the cow.
The cow is big.
("cow" "is" "big" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is round.
("cow" "is" "round" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow does not visit the dog.
("cow" "visits" "dog" "-")
The dog is round.
("dog" "is" "round" "+")
The dog does not see the cow.
("dog" "sees" "cow" "-")
If something is red then it does not need the dog.
((("something" "is" "red" "+")) -> ("something" "needs" "dog" "-"))
If something sees the dog then it needs the dog.
((("something" "sees" "dog" "+")) -> ("something" "needs" "dog" "+"))
If the cow needs the dog then the dog visits the cow.
((("cow" "needs" "dog" "+")) -> ("dog" "visits" "cow" "+"))
If something sees the dog and it needs the cow then it is not kind.
((("something" "sees" "dog" "+") ("something" "needs" "cow" "+")) -> ("something" "is" "kind" "-"))
If something is big and it does not need the dog then it does not need the cow.
((("something" "is" "big" "+") ("something" "needs" "dog" "~")) -> ("something" "needs" "cow" "-"))
If something visits the dog then it does not need the cow.
((("something" "visits" "dog" "+")) -> ("something" "needs" "cow" "-"))
The cow does not visit the dog.
True
1
proof
[(triple5)]
("cow" "visits" "dog" "-")
triple5
The cow visits the dog.
False
1
inv-proof
[(triple5)]
("cow" "visits" "dog" "+")
triple5
The cow needs the dog.
True
2
proof
[(((triple4) -> rule2))]
("cow" "needs" "dog" "+")
((triple4) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The cow does not need the dog.
False
2
inv-proof
[(((triple4) -> rule2))]
("cow" "needs" "dog" "-")
((triple4) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The dog visits the cow.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("dog" "visits" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The dog does not visit the cow.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("dog" "visits" "cow" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2
The dog does not need the dog.
Unknown
inv-rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "needs" "dog" "-")
The dog is red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
The dog does not need the cow.
Unknown
inv-random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow does not visit the dog.[(triple5)] The cow is big.[(triple1)] The cow is nice.[(triple2)] The cow is round.[(triple3)] The cow sees the dog.[(triple4)] The dog does not see the cow.[(triple7)] The dog is round.[(triple6)] @1: The cow needs the dog.[(((triple4) -> rule2))] @2: The dog visits the cow.[(((((triple4) -> rule2)) -> rule3))]
The cow does not visit the dog.
("cow" "visits" "dog" "-")
triple5
The cow is big.
("cow" "is" "big" "+")
triple1
The cow is nice.
("cow" "is" "nice" "+")
triple2
The cow is round.
("cow" "is" "round" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
The dog does not see the cow.
("dog" "sees" "cow" "-")
triple7
The dog is round.
("dog" "is" "round" "+")
triple6
The cow needs the dog.
("cow" "needs" "dog" "+")
((triple4) -> (rule2 % int1))
The cow needs the dog.
("cow" "needs" "dog" "+")
int1
The dog visits the cow.
("dog" "visits" "cow" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the cow.
("dog" "visits" "cow" "+")
int1
The cow needs the dog.
("cow" "needs" "dog" "+")
int2