The dog eats the lion. The lion is round. The mouse is blue. If something is blue and it visits the mouse then it is round. If something chases the dog and the dog is green then the dog is cold. If something is round then it chases the lion. If something eats the lion then the lion visits the dog. If something visits the dog then the dog is cold. If something eats the mouse then the mouse chases the lion. If something visits the lion then the lion is round. If something chases the dog and it chases the lion then the lion chases the mouse.
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion is round.
("lion" "is" "round" "+")
The mouse is blue.
("mouse" "is" "blue" "+")
If something is blue and it visits the mouse then it is round.
((("something" "is" "blue" "+") ("something" "visits" "mouse" "+")) -> ("something" "is" "round" "+"))
If something chases the dog and the dog is green then the dog is cold.
((("something" "chases" "dog" "+") ("dog" "is" "green" "+")) -> ("dog" "is" "cold" "+"))
If something is round then it chases the lion.
((("something" "is" "round" "+")) -> ("something" "chases" "lion" "+"))
If something eats the lion then the lion visits the dog.
((("something" "eats" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If something visits the dog then the dog is cold.
((("something" "visits" "dog" "+")) -> ("dog" "is" "cold" "+"))
If something eats the mouse then the mouse chases the lion.
((("something" "eats" "mouse" "+")) -> ("mouse" "chases" "lion" "+"))
If something visits the lion then the lion is round.
((("something" "visits" "lion" "+")) -> ("lion" "is" "round" "+"))
If something chases the dog and it chases the lion then the lion chases the mouse.
((("something" "chases" "dog" "+") ("something" "chases" "lion" "+")) -> ("lion" "chases" "mouse" "+"))
The mouse is blue.
True
1
proof
[(triple3)]
("mouse" "is" "blue" "+")
triple3
The dog does not eat the lion.
False
1
inv-proof
[(triple1)]
("dog" "eats" "lion" "-")
triple1
The lion visits the dog.
True
2
proof
[(((triple1) -> rule4))]
("lion" "visits" "dog" "+")
((triple1) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion does not visit the dog.
False
2
inv-proof
[(((triple1) -> rule4))]
("lion" "visits" "dog" "-")
((triple1) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The dog is cold.
True
3
proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The dog is not cold.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule5))]
("dog" "is" "cold" "-")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The mouse does not chase the lion.
Unknown
inv-rconc
[@2: The mouse chases the lion.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("mouse" "chases" "lion" "-")
The lion chases the mouse.
Unknown
rconc
[@1: The lion chases the mouse.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "chases" "mouse" "+")
The mouse is not round.
Unknown
inv-rconc
[@1: The mouse is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "round" "-")
The dog visits the mouse.
Unknown
random
[@0: The dog visits the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "mouse" "+")
The lion does not visit the lion.
Unknown
inv-random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "-")
The dog is blue.
Unknown
random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "+")
@0: The dog eats the lion.[(triple1)] The lion is round.[(triple2)] The mouse is blue.[(triple3)] @1: The lion chases the lion.[(((triple2) -> rule3))] The lion visits the dog.[(((triple1) -> rule4))] @2: The dog is cold.[(((((triple1) -> rule4)) -> rule5))]
The dog eats the lion.
("dog" "eats" "lion" "+")
triple1
The lion is round.
("lion" "is" "round" "+")
triple2
The mouse is blue.
("mouse" "is" "blue" "+")
triple3
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple2) -> (rule3 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple1) -> (rule4 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
((((triple1) -> (rule4 % int2))) -> (rule5 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2