The dog sees the lion. The lion is young. If the lion visits the dog and the lion eats the dog then the lion is blue. If something is young then it sees the dog. If the dog visits the lion then the dog sees the lion. If something sees the lion then it visits the dog. If something visits the dog then it sees the dog. If something is big then it eats the dog.
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion is young.
("lion" "is" "young" "+")
If the lion visits the dog and the lion eats the dog then the lion is blue.
((("lion" "visits" "dog" "+") ("lion" "eats" "dog" "+")) -> ("lion" "is" "blue" "+"))
If something is young then it sees the dog.
((("something" "is" "young" "+")) -> ("something" "sees" "dog" "+"))
If the dog visits the lion then the dog sees the lion.
((("dog" "visits" "lion" "+")) -> ("dog" "sees" "lion" "+"))
If something sees the lion then it visits the dog.
((("something" "sees" "lion" "+")) -> ("something" "visits" "dog" "+"))
If something visits the dog then it sees the dog.
((("something" "visits" "dog" "+")) -> ("something" "sees" "dog" "+"))
If something is big then it eats the dog.
((("something" "is" "big" "+")) -> ("something" "eats" "dog" "+"))
The lion is young.
True
1
proof
[(triple2)]
("lion" "is" "young" "+")
triple2
The dog does not see the lion.
False
1
inv-proof
[(triple1)]
("dog" "sees" "lion" "-")
triple1
The lion sees the dog.
True
2
proof
[(((triple2) -> rule2))]
("lion" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion does not see the dog.
False
2
inv-proof
[(((triple2) -> rule2))]
("lion" "sees" "dog" "-")
((triple2) -> (rule2 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog sees the dog.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "sees" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not see the dog.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "sees" "dog" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2
The dog does not eat the dog.
Unknown
inv-rconc
[@1: The dog eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "eats" "dog" "-")
The lion is blue.
Unknown
rconc
[@2: The lion is blue.[CWA. Example of deepest failure = (rule1 <- rule4 <- FAIL)]]
("lion" "is" "blue" "+")
The lion does not eat the dog.
Unknown
inv-rconc
[@1: The lion eats the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "eats" "dog" "-")
The lion is rough.
Unknown
random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "+")
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 dog eats the lion.
Unknown
random
[@0: The dog eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "lion" "+")
@0: The dog sees the lion.[(triple1)] The lion is young.[(triple2)] @1: The dog visits the dog.[(((triple1) -> rule4))] The lion sees the dog.[(((triple2) -> rule2))] @2: The dog sees the dog.[(((((triple1) -> rule4)) -> rule5))]
The dog sees the lion.
("dog" "sees" "lion" "+")
triple1
The lion is young.
("lion" "is" "young" "+")
triple2
The dog visits the dog.
("dog" "visits" "dog" "+")
((triple1) -> (rule4 % int1))
The dog visits the dog.
("dog" "visits" "dog" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple2) -> (rule2 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog visits the dog.
("dog" "visits" "dog" "+")
int2