The dog eats the lion. The lion is red. The lion visits the dog. If the lion sees the dog and the lion eats the dog then the lion is cold. If someone visits the dog and the dog eats the lion then the dog sees the lion. If the dog sees the lion then the dog visits the lion.
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion is red.
("lion" "is" "red" "+")
The lion visits the dog.
("lion" "visits" "dog" "+")
If the lion sees the dog and the lion eats the dog then the lion is cold.
((("lion" "sees" "dog" "+") ("lion" "eats" "dog" "+")) -> ("lion" "is" "cold" "+"))
If someone visits the dog and the dog eats the lion then the dog sees the lion.
((("someone" "visits" "dog" "+") ("dog" "eats" "lion" "+")) -> ("dog" "sees" "lion" "+"))
If the dog sees the lion then the dog visits the lion.
((("dog" "sees" "lion" "+")) -> ("dog" "visits" "lion" "+"))
The dog eats the lion.
True
1
proof
[(triple1)]
("dog" "eats" "lion" "+")
triple1
The lion does not visit the dog.
False
1
inv-proof
[(triple3)]
("lion" "visits" "dog" "-")
triple3
The dog sees the lion.
True
3
proof
[(((triple3 triple1) -> rule2))]
("dog" "sees" "lion" "+")
((triple3 triple1) -> (rule2 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog does not see the lion.
False
3
inv-proof
[(((triple3 triple1) -> rule2))]
("dog" "sees" "lion" "-")
((triple3 triple1) -> (rule2 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog visits the lion.
True
4
proof
[(((((triple3 triple1) -> rule2)) -> rule3))]
("dog" "visits" "lion" "+")
((((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The dog does not visit the lion.
False
4
inv-proof
[(((((triple3 triple1) -> rule2)) -> rule3))]
("dog" "visits" "lion" "-")
((((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2
The lion is not cold.
Unknown
inv-rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "cold" "-")
The lion sees the dog.
Unknown
random
[@0: The lion sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "dog" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The lion is big.
Unknown
random
[@0: The lion is big.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "big" "+")
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 red.
Unknown
random
[@0: The dog is red.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "red" "+")
@0: The dog eats the lion.[(triple1)] The lion is red.[(triple2)] The lion visits the dog.[(triple3)] @1: The dog sees the lion.[(((triple3 triple1) -> rule2))] @2: The dog visits the lion.[(((((triple3 triple1) -> rule2)) -> rule3))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The lion is red.
("lion" "is" "red" "+")
triple2
The lion visits the dog.
("lion" "visits" "dog" "+")
triple3
The dog sees the lion.
("dog" "sees" "lion" "+")
((triple3 triple1) -> (rule2 % int1))
The dog sees the lion.
("dog" "sees" "lion" "+")
int1
The dog visits the lion.
("dog" "visits" "lion" "+")
((((triple3 triple1) -> (rule2 % int2))) -> (rule3 % int1))
The dog visits the lion.
("dog" "visits" "lion" "+")
int1
The dog sees the lion.
("dog" "sees" "lion" "+")
int2