The cat is cold. The cow likes the cat. The dog needs the cow. If the cat eats the cow then the cat likes the dog. If something is young and it does not like the cat then the cat needs the cow. If something likes the dog then the dog does not eat the cow. If something is rough and it does not need the dog then the dog does not need the cat. If something likes the cat then the cat eats the cow. If something is cold then it needs the cow. If something likes the dog and the dog likes the cow then the dog is blue. If something needs the cat and it eats the cow then the cat is blue.
The cat is cold.
("cat" "is" "cold" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
If the cat eats the cow then the cat likes the dog.
((("cat" "eats" "cow" "+")) -> ("cat" "likes" "dog" "+"))
If something is young and it does not like the cat then the cat needs the cow.
((("something" "is" "young" "+") ("something" "likes" "cat" "~")) -> ("cat" "needs" "cow" "+"))
If something likes the dog then the dog does not eat the cow.
((("something" "likes" "dog" "+")) -> ("dog" "eats" "cow" "-"))
If something is rough and it does not need the dog then the dog does not need the cat.
((("something" "is" "rough" "+") ("something" "needs" "dog" "~")) -> ("dog" "needs" "cat" "-"))
If something likes the cat then the cat eats the cow.
((("something" "likes" "cat" "+")) -> ("cat" "eats" "cow" "+"))
If something is cold then it needs the cow.
((("something" "is" "cold" "+")) -> ("something" "needs" "cow" "+"))
If something likes the dog and the dog likes the cow then the dog is blue.
((("something" "likes" "dog" "+") ("dog" "likes" "cow" "+")) -> ("dog" "is" "blue" "+"))
If something needs the cat and it eats the cow then the cat is blue.
((("something" "needs" "cat" "+") ("something" "eats" "cow" "+")) -> ("cat" "is" "blue" "+"))
The cat is cold.
True
1
proof
[(triple1)]
("cat" "is" "cold" "+")
triple1
The cow does not like the cat.
False
1
inv-proof
[(triple2)]
("cow" "likes" "cat" "-")
triple2
The cat needs the cow.
True
2
proof
[(((triple1) -> rule6))]
("cat" "needs" "cow" "+")
((triple1) -> (rule6 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat does not need the cow.
False
2
inv-proof
[(((triple1) -> rule6))]
("cat" "needs" "cow" "-")
((triple1) -> (rule6 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat likes the dog.
True
3
proof
[(((((triple2) -> rule5)) -> rule1))]
("cat" "likes" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat does not like the dog.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule1))]
("cat" "likes" "dog" "-")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cat" "is" "blue" "-")
The dog is blue.
Unknown
rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "blue" "+")
The cow does not need the cow.
Unknown
inv-rconc
[@1: The cow needs the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "needs" "cow" "-")
The cat is round.
Unknown
random
[@0: The cat is round.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "round" "+")
The cat does not eat the cat.
Unknown
inv-random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "-")
The cow likes the cow.
Unknown
random
[@0: The cow likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "cow" "+")
@0: The cat is cold.[(triple1)] The cow likes the cat.[(triple2)] The dog needs the cow.[(triple3)] @1: The cat eats the cow.[(((triple2) -> rule5))] The cat needs the cow.[(((triple1) -> rule6))] @2: The cat likes the dog.[(((((triple2) -> rule5)) -> rule1))] @3: The dog does not eat the cow.[(((((((triple2) -> rule5)) -> rule1)) -> rule3))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple2
The dog needs the cow.
("dog" "needs" "cow" "+")
triple3
The cat eats the cow.
("cat" "eats" "cow" "+")
((triple2) -> (rule5 % int1))
The cat eats the cow.
("cat" "eats" "cow" "+")
int1
The cat needs the cow.
("cat" "needs" "cow" "+")
((triple1) -> (rule6 % int1))
The cat needs the cow.
("cat" "needs" "cow" "+")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
((((triple2) -> (rule5 % int2))) -> (rule1 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The cat eats the cow.
("cat" "eats" "cow" "+")
int2
The dog does not eat the cow.
("dog" "eats" "cow" "-")
((((((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
The dog does not eat the cow.
("dog" "eats" "cow" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat eats the cow.
("cat" "eats" "cow" "+")
int3