The cat visits the dog. The dog needs the cat. The lion visits the cat. If the dog needs the cat and the dog visits the cat then the cat sees the lion. If someone needs the cat then they visit the cat. If someone needs the lion and the lion is blue then the lion is green. If someone needs the dog and they need the lion then the lion visits the dog. If someone sees the lion then they need the cat. If someone visits the cat and they see the dog then they are cold.
The cat visits the dog.
("cat" "visits" "dog" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
If the dog needs the cat and the dog visits the cat then the cat sees the lion.
((("dog" "needs" "cat" "+") ("dog" "visits" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If someone needs the cat then they visit the cat.
((("someone" "needs" "cat" "+")) -> ("someone" "visits" "cat" "+"))
If someone needs the lion and the lion is blue then the lion is green.
((("someone" "needs" "lion" "+") ("lion" "is" "blue" "+")) -> ("lion" "is" "green" "+"))
If someone needs the dog and they need the lion then the lion visits the dog.
((("someone" "needs" "dog" "+") ("someone" "needs" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If someone sees the lion then they need the cat.
((("someone" "sees" "lion" "+")) -> ("someone" "needs" "cat" "+"))
If someone visits the cat and they see the dog then they are cold.
((("someone" "visits" "cat" "+") ("someone" "sees" "dog" "+")) -> ("someone" "is" "cold" "+"))
The lion visits the cat.
True
1
proof
[(triple3)]
("lion" "visits" "cat" "+")
triple3
The lion does not visit the cat.
False
1
inv-proof
[(triple3)]
("lion" "visits" "cat" "-")
triple3
The dog visits the cat.
True
2
proof
[(((triple2) -> rule2))]
("dog" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The dog does not visit the cat.
False
2
inv-proof
[(((triple2) -> rule2))]
("dog" "visits" "cat" "-")
((triple2) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat sees the lion.
True
4
proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("cat" "sees" "lion" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat does not see the lion.
False
4
inv-proof
[(((triple2 ((triple2) -> rule2)) -> rule1))]
("cat" "sees" "lion" "-")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat needs the cat.
True
5
proof
[(((((triple2 ((triple2) -> rule2)) -> rule1)) -> rule5))]
("cat" "needs" "cat" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The cat does not need the cat.
False
5
inv-proof
[(((((triple2 ((triple2) -> rule2)) -> rule1)) -> rule5))]
("cat" "needs" "cat" "-")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The lion does not need the cat.
Unknown
inv-rconc
[@1: The lion needs the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "cat" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "cold" "+")
The dog is not cold.
Unknown
inv-rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "cold" "-")
The lion is green.
Unknown
rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "green" "+")
The lion is not young.
Unknown
inv-random
[@0: The lion is young.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "young" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The dog is green.
Unknown
random
[@0: The dog is green.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "green" "+")
@0: The cat visits the dog.[(triple1)] The dog needs the cat.[(triple2)] The lion visits the cat.[(triple3)] @1: The dog visits the cat.[(((triple2) -> rule2))] @2: The cat sees the lion.[(((triple2 ((triple2) -> rule2)) -> rule1))] @3: The cat needs the cat.[(((((triple2 ((triple2) -> rule2)) -> rule1)) -> rule5))] @4: The cat visits the cat.[(((((((triple2 ((triple2) -> rule2)) -> rule1)) -> rule5)) -> rule2))]
The cat visits the dog.
("cat" "visits" "dog" "+")
triple1
The dog needs the cat.
("dog" "needs" "cat" "+")
triple2
The lion visits the cat.
("lion" "visits" "cat" "+")
triple3
The dog visits the cat.
("dog" "visits" "cat" "+")
((triple2) -> (rule2 % int1))
The dog visits the cat.
("dog" "visits" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
((triple2 ((triple2) -> (rule2 % int2))) -> (rule1 % int1))
The cat sees the lion.
("cat" "sees" "lion" "+")
int1
The dog visits the cat.
("dog" "visits" "cat" "+")
int2
The cat needs the cat.
("cat" "needs" "cat" "+")
((((triple2 ((triple2) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
The cat needs the cat.
("cat" "needs" "cat" "+")
int1
The cat sees the lion.
("cat" "sees" "lion" "+")
int2
The dog visits the cat.
("dog" "visits" "cat" "+")
int3
The cat visits the cat.
("cat" "visits" "cat" "+")
((((((triple2 ((triple2) -> (rule2 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat needs the cat.
("cat" "needs" "cat" "+")
int2
The cat sees the lion.
("cat" "sees" "lion" "+")
int3
The dog visits the cat.
("dog" "visits" "cat" "+")
int4