The dog is green. The dog sees the mouse. The dog sees the tiger. The lion chases the dog. The lion eats the tiger. The mouse is big. The mouse is cold. The tiger chases the dog. The tiger chases the lion. The tiger eats the dog. The tiger eats the lion. The tiger is blue. If something is blue and young then it sees the lion. If something eats the mouse then it chases the lion. If something chases the lion and it is big then the lion is cold. If something is big and it chases the mouse then it eats the mouse. If something is big then it eats the lion. If something eats the lion and the lion chases the dog then it sees the mouse.
The dog is green.
("dog" "is" "green" "+")
The dog sees the mouse.
("dog" "sees" "mouse" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion eats the tiger.
("lion" "eats" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse is cold.
("mouse" "is" "cold" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger chases the lion.
("tiger" "chases" "lion" "+")
The tiger eats the dog.
("tiger" "eats" "dog" "+")
The tiger eats the lion.
("tiger" "eats" "lion" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
If something is blue and young then it sees the lion.
((("something" "is" "blue" "+") ("something" "is" "young" "+")) -> ("something" "sees" "lion" "+"))
If something eats the mouse then it chases the lion.
((("something" "eats" "mouse" "+")) -> ("something" "chases" "lion" "+"))
If something chases the lion and it is big then the lion is cold.
((("something" "chases" "lion" "+") ("something" "is" "big" "+")) -> ("lion" "is" "cold" "+"))
If something is big and it chases the mouse then it eats the mouse.
((("something" "is" "big" "+") ("something" "chases" "mouse" "+")) -> ("something" "eats" "mouse" "+"))
If something is big then it eats the lion.
((("something" "is" "big" "+")) -> ("something" "eats" "lion" "+"))
If something eats the lion and the lion chases the dog then it sees the mouse.
((("something" "eats" "lion" "+") ("lion" "chases" "dog" "+")) -> ("something" "sees" "mouse" "+"))
The tiger chases the lion.
True
1
proof
[(triple9)]
("tiger" "chases" "lion" "+")
triple9
The dog does not see the mouse.
False
1
inv-proof
[(triple2)]
("dog" "sees" "mouse" "-")
triple2
The mouse eats the lion.
True
2
proof
[(((triple6) -> rule5))]
("mouse" "eats" "lion" "+")
((triple6) -> (rule5 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse does not eat the lion.
False
2
inv-proof
[(((triple6) -> rule5))]
("mouse" "eats" "lion" "-")
((triple6) -> (rule5 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The mouse sees the mouse.
True
4
proof
[(((((triple6) -> rule5) triple4) -> rule6))]
("mouse" "sees" "mouse" "+")
((((triple6) -> (rule5 % int2)) triple4) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The mouse does not see the mouse.
False
4
inv-proof
[(((((triple6) -> rule5) triple4) -> rule6))]
("mouse" "sees" "mouse" "-")
((((triple6) -> (rule5 % int2)) triple4) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2
The tiger does not eat the mouse.
Unknown
inv-rconc
[@1: The tiger eats the mouse.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "mouse" "-")
The dog chases the lion.
Unknown
rconc
[@2: The dog chases the lion.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("dog" "chases" "lion" "+")
The lion does not see the mouse.
Unknown
inv-rconc
[@2: The lion sees the mouse.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("lion" "sees" "mouse" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The dog is not blue.
Unknown
inv-random
[@0: The dog is blue.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "blue" "-")
The lion sees the dog.
Unknown
random
[@0: The lion sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "dog" "+")
@0: The dog is green.[(triple1)] The dog sees the mouse.[(triple2)] The dog sees the tiger.[(triple3)] The lion chases the dog.[(triple4)] The lion eats the tiger.[(triple5)] The mouse is big.[(triple6)] The mouse is cold.[(triple7)] The tiger chases the dog.[(triple8)] The tiger chases the lion.[(triple9)] The tiger eats the dog.[(triple10)] The tiger eats the lion.[(triple11)] The tiger is blue.[(triple12)] @1: The mouse eats the lion.[(((triple6) -> rule5))] The tiger sees the mouse.[(((triple11 triple4) -> rule6))] @2: The mouse sees the mouse.[(((((triple6) -> rule5) triple4) -> rule6))]
The dog is green.
("dog" "is" "green" "+")
triple1
The dog sees the mouse.
("dog" "sees" "mouse" "+")
triple2
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple3
The lion chases the dog.
("lion" "chases" "dog" "+")
triple4
The lion eats the tiger.
("lion" "eats" "tiger" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse is cold.
("mouse" "is" "cold" "+")
triple7
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple8
The tiger chases the lion.
("tiger" "chases" "lion" "+")
triple9
The tiger eats the dog.
("tiger" "eats" "dog" "+")
triple10
The tiger eats the lion.
("tiger" "eats" "lion" "+")
triple11
The tiger is blue.
("tiger" "is" "blue" "+")
triple12
The mouse eats the lion.
("mouse" "eats" "lion" "+")
((triple6) -> (rule5 % int1))
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int1
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
((triple11 triple4) -> (rule6 % int1))
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
int1
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple6) -> (rule5 % int2)) triple4) -> (rule6 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse eats the lion.
("mouse" "eats" "lion" "+")
int2