The cat is nice. The cat does not like the lion. The cat does not need the lion. The cat does not visit the lion. The cow is cold. The cow is green. The cow is rough. The cow is round. The cow likes the cat. The cow likes the lion. The cow needs the lion. The cow does not visit the cat. The cow does not visit the lion. The lion is nice. The lion is not rough. The lion visits the cat. If someone needs the lion and the lion visits the cow then the lion needs the cat. If the lion is rough then the lion needs the cat. If someone is nice then they like the cat. If someone is green then they are round. If the lion likes the cat then the cat visits the cow. If someone needs the cow then the cow likes the cat.
The cat is nice.
("cat" "is" "nice" "+")
The cat does not like the lion.
("cat" "likes" "lion" "-")
The cat does not need the lion.
("cat" "needs" "lion" "-")
The cat does not visit the lion.
("cat" "visits" "lion" "-")
The cow is cold.
("cow" "is" "cold" "+")
The cow is green.
("cow" "is" "green" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow is round.
("cow" "is" "round" "+")
The cow likes the cat.
("cow" "likes" "cat" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow does not visit the cat.
("cow" "visits" "cat" "-")
The cow does not visit the lion.
("cow" "visits" "lion" "-")
The lion is nice.
("lion" "is" "nice" "+")
The lion is not rough.
("lion" "is" "rough" "-")
The lion visits the cat.
("lion" "visits" "cat" "+")
If someone needs the lion and the lion visits the cow then the lion needs the cat.
((("someone" "needs" "lion" "+") ("lion" "visits" "cow" "+")) -> ("lion" "needs" "cat" "+"))
If the lion is rough then the lion needs the cat.
((("lion" "is" "rough" "+")) -> ("lion" "needs" "cat" "+"))
If someone is nice then they like the cat.
((("someone" "is" "nice" "+")) -> ("someone" "likes" "cat" "+"))
If someone is green then they are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If the lion likes the cat then the cat visits the cow.
((("lion" "likes" "cat" "+")) -> ("cat" "visits" "cow" "+"))
If someone needs the cow then the cow likes the cat.
((("someone" "needs" "cow" "+")) -> ("cow" "likes" "cat" "+"))
The cat is nice.
True
1
proof
[(triple1)]
("cat" "is" "nice" "+")
triple1
The cow visits the cat.
False
1
inv-proof
[(triple12)]
("cow" "visits" "cat" "+")
triple12
The cat likes the cat.
True
2
proof
[(((triple1) -> rule3))]
("cat" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion does not like the cat.
False
2
inv-proof
[(((triple14) -> rule3))]
("lion" "likes" "cat" "-")
((triple14) -> (rule3 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cat visits the cow.
True
3
proof
[(((((triple14) -> rule3)) -> rule5))]
("cat" "visits" "cow" "+")
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The cat does not visit the cow.
False
3
inv-proof
[(((((triple14) -> rule3)) -> rule5))]
("cat" "visits" "cow" "-")
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion does not need the cat.
Unknown
inv-rconc
[@1: The lion needs the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "needs" "cat" "-")
The lion is round.
Unknown
rconc
[@1: The lion is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "round" "+")
The cat is not round.
Unknown
inv-rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "round" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The cow needs the cat.
Unknown
random
[@0: The cow needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cat" "+")
@0: The cat does not like the lion.[(triple2)] The cat does not need the lion.[(triple3)] The cat does not visit the lion.[(triple4)] The cat is nice.[(triple1)] The cow does not visit the cat.[(triple12)] The cow does not visit the lion.[(triple13)] The cow is cold.[(triple5)] The cow is green.[(triple6)] The cow is rough.[(triple7)] The cow is round.[(triple8 OR ((triple6) -> rule4))] The cow likes the cat.[(triple9)] The cow likes the lion.[(triple10)] The cow needs the lion.[(triple11)] The lion is nice.[(triple14)] The lion is not rough.[(triple15)] The lion visits the cat.[(triple16)] @1: The cat likes the cat.[(((triple1) -> rule3))] The lion likes the cat.[(((triple14) -> rule3))] @2: The cat visits the cow.[(((((triple14) -> rule3)) -> rule5))]
The cat does not like the lion.
("cat" "likes" "lion" "-")
triple2
The cat does not need the lion.
("cat" "needs" "lion" "-")
triple3
The cat does not visit the lion.
("cat" "visits" "lion" "-")
triple4
The cat is nice.
("cat" "is" "nice" "+")
triple1
The cow does not visit the cat.
("cow" "visits" "cat" "-")
triple12
The cow does not visit the lion.
("cow" "visits" "lion" "-")
triple13
The cow is cold.
("cow" "is" "cold" "+")
triple5
The cow is green.
("cow" "is" "green" "+")
triple6
The cow is rough.
("cow" "is" "rough" "+")
triple7
The cow is round.
("cow" "is" "round" "+")
triple8
((triple6) -> (rule4 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
triple9
The cow likes the lion.
("cow" "likes" "lion" "+")
triple10
The cow needs the lion.
("cow" "needs" "lion" "+")
triple11
The lion is nice.
("lion" "is" "nice" "+")
triple14
The lion is not rough.
("lion" "is" "rough" "-")
triple15
The lion visits the cat.
("lion" "visits" "cat" "+")
triple16
The cat likes the cat.
("cat" "likes" "cat" "+")
((triple1) -> (rule3 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
((triple14) -> (rule3 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cat visits the cow.
("cat" "visits" "cow" "+")
((((triple14) -> (rule3 % int2))) -> (rule5 % int1))
The cat visits the cow.
("cat" "visits" "cow" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2