The cat is big. The cat needs the dog. The cat visits the dog. The dog is rough. The dog likes the cat. The dog needs the cat. The dog visits the cat. If someone likes the dog then they do not visit the cat. If someone needs the cat and the cat is not rough then they do not like the cat. If someone likes the cat then the cat needs the dog. If someone visits the dog then they like the dog. If someone likes the cat and the cat does not visit the dog then they are blue. If someone needs the dog then the dog is cold. If someone needs the dog and they visit the cat then they are not cold. If the cat does not need the dog then the dog is not young.
The cat is big.
("cat" "is" "big" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
If someone likes the dog then they do not visit the cat.
((("someone" "likes" "dog" "+")) -> ("someone" "visits" "cat" "-"))
If someone needs the cat and the cat is not rough then they do not like the cat.
((("someone" "needs" "cat" "+") ("cat" "is" "rough" "~")) -> ("someone" "likes" "cat" "-"))
If someone likes the cat then the cat needs the dog.
((("someone" "likes" "cat" "+")) -> ("cat" "needs" "dog" "+"))
If someone visits the dog then they like the dog.
((("someone" "visits" "dog" "+")) -> ("someone" "likes" "dog" "+"))
If someone likes the cat and the cat does not visit the dog then they are blue.
((("someone" "likes" "cat" "+") ("cat" "visits" "dog" "~")) -> ("someone" "is" "blue" "+"))
If someone needs the dog then the dog is cold.
((("someone" "needs" "dog" "+")) -> ("dog" "is" "cold" "+"))
If someone needs the dog and they visit the cat then they are not cold.
((("someone" "needs" "dog" "+") ("someone" "visits" "cat" "+")) -> ("someone" "is" "cold" "-"))
If the cat does not need the dog then the dog is not young.
((("cat" "needs" "dog" "~")) -> ("dog" "is" "young" "-"))
The dog likes the cat.
True
1
proof
[(triple5)]
("dog" "likes" "cat" "+")
triple5
The cat does not visit the dog.
False
1
inv-proof
[(triple3)]
("cat" "visits" "dog" "-")
triple3
The dog is cold.
True
2
proof
[(((triple2) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("dog" "is" "cold" "+")
((triple2) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The dog is not cold.
False
2
inv-proof
[(((triple2) -> rule6) OR ((((triple5) -> rule3)) -> rule6))]
("dog" "is" "cold" "-")
((triple2) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat does not visit the cat.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("cat" "visits" "cat" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat visits the cat.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("cat" "visits" "cat" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2
The cat is not blue.
Unknown
inv-rconc
[@1: The cat is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "blue" "-")
The dog likes the dog.
Unknown
rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "likes" "dog" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "blue" "-")
The dog is young.
Unknown
random
[@0: The dog is young.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "young" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The cat is cold.
Unknown
random
[@0: The cat is cold.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "cold" "+")
@0: The cat is big.[(triple1)] The cat needs the dog.[(triple2 OR ((triple5) -> rule3))] The cat visits the dog.[(triple3)] The dog is rough.[(triple4)] The dog likes the cat.[(triple5)] The dog needs the cat.[(triple6)] The dog visits the cat.[(triple7)] @1: The cat likes the dog.[(((triple3) -> rule4))] The dog is cold.[(((triple2) -> rule6) OR ((((triple5) -> rule3)) -> rule6))] @2: The cat does not visit the cat.[(((((triple3) -> rule4)) -> rule1))]
The cat is big.
("cat" "is" "big" "+")
triple1
The cat needs the dog.
("cat" "needs" "dog" "+")
triple2
((triple5) -> (rule3 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the dog.
("cat" "visits" "dog" "+")
triple3
The dog is rough.
("dog" "is" "rough" "+")
triple4
The dog likes the cat.
("dog" "likes" "cat" "+")
triple5
The dog needs the cat.
("dog" "needs" "cat" "+")
triple6
The dog visits the cat.
("dog" "visits" "cat" "+")
triple7
The cat likes the dog.
("cat" "likes" "dog" "+")
((triple3) -> (rule4 % int1))
The cat likes the dog.
("cat" "likes" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((triple2) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat does not visit the cat.
("cat" "visits" "cat" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The cat does not visit the cat.
("cat" "visits" "cat" "-")
int1
The cat likes the dog.
("cat" "likes" "dog" "+")
int2