The cat does not visit the dog. The cow likes the cat. The dog is green. If something likes the cat then it does not like the dog. If something is big and it does not like the cat then it is green. If something likes the cat then the cat likes the cow. If something sees the dog then the dog is green. If something sees the cow then it does not see the cat. If something is big then it likes the cow. If the cat does not visit the dog then the cat does not like the dog. If something likes the cow then it visits the cow.
The cat does not visit the dog.
("cat" "visits" "dog" "-")
The cow likes the cat.
("cow" "likes" "cat" "+")
The dog is green.
("dog" "is" "green" "+")
If something likes the cat then it does not like the dog.
((("something" "likes" "cat" "+")) -> ("something" "likes" "dog" "-"))
If something is big and it does not like the cat then it is green.
((("something" "is" "big" "+") ("something" "likes" "cat" "~")) -> ("something" "is" "green" "+"))
If something likes the cat then the cat likes the cow.
((("something" "likes" "cat" "+")) -> ("cat" "likes" "cow" "+"))
If something sees the dog then the dog is green.
((("something" "sees" "dog" "+")) -> ("dog" "is" "green" "+"))
If something sees the cow then it does not see the cat.
((("something" "sees" "cow" "+")) -> ("something" "sees" "cat" "-"))
If something is big then it likes the cow.
((("something" "is" "big" "+")) -> ("something" "likes" "cow" "+"))
If the cat does not visit the dog then the cat does not like the dog.
((("cat" "visits" "dog" "~")) -> ("cat" "likes" "dog" "-"))
If something likes the cow then it visits the cow.
((("something" "likes" "cow" "+")) -> ("something" "visits" "cow" "+"))
The cat does not visit the dog.
True
1
proof
[(triple1)]
("cat" "visits" "dog" "-")
triple1
The cow does not like the cat.
False
1
inv-proof
[(triple2)]
("cow" "likes" "cat" "-")
triple2
The cat does not like the dog.
True
2
proof
[(((triple1) -> rule7))]
("cat" "likes" "dog" "-")
((triple1) -> (rule7 % int1))
The cat does not like the dog.
("cat" "likes" "dog" "-")
int1
The cat does not like the cow.
False
2
inv-proof
[(((triple2) -> rule3))]
("cat" "likes" "cow" "-")
((triple2) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cat visits the cow.
True
3
proof
[(((((triple2) -> rule3)) -> rule8))]
("cat" "visits" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cat does not visit the cow.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule8))]
("cat" "visits" "cow" "-")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "likes" "cow" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "green" "+")
The cow does not visit the cow.
Unknown
inv-rconc
[@2: The cow visits the cow.[CWA. Example of deepest failure = (rule8 <- rule6 <- FAIL)]]
("cow" "visits" "cow" "-")
The cow is cold.
Unknown
random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The cat is kind.
Unknown
random
[@0: The cat is kind.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "kind" "+")
@0: The cat does not visit the dog.[(triple1)] The cow likes the cat.[(triple2)] The dog is green.[(triple3)] @1: The cat does not like the dog.[(((triple1) -> rule7))] The cat likes the cow.[(((triple2) -> rule3))] The cow does not like the dog.[(((triple2) -> rule1))] @2: The cat visits the cow.[(((((triple2) -> rule3)) -> rule8))]
The cat does not visit the dog.
("cat" "visits" "dog" "-")
triple1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The dog is green.
("dog" "is" "green" "+")
triple3
The cat does not like the dog.
("cat" "likes" "dog" "-")
((triple1) -> (rule7 % int1))
The cat does not like the dog.
("cat" "likes" "dog" "-")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
((triple2) -> (rule3 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow does not like the dog.
("cow" "likes" "dog" "-")
((triple2) -> (rule1 % int1))
The cow does not like the dog.
("cow" "likes" "dog" "-")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
((((triple2) -> (rule3 % int2))) -> (rule8 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2