The dog chases the mouse. The dog needs the lion. The dog needs the mouse. The lion chases the dog. The lion likes the dog. The lion likes the mouse. The mouse chases the lion. The mouse is kind. The mouse likes the dog. The mouse does not need the lion. If the lion needs the mouse then the lion likes the mouse. If the dog is blue then the dog likes the mouse. If the lion does not like the dog and the dog does not need the mouse then the dog does not need the lion. If something is cold then it chases the dog. If something is kind and it chases the lion then it chases the dog. If something is cold then it needs the dog. If something needs the mouse and the mouse chases the lion then it is blue. If something likes the mouse then it chases the lion.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion likes the dog.
("lion" "likes" "dog" "+")
The lion likes the mouse.
("lion" "likes" "mouse" "+")
The mouse chases the lion.
("mouse" "chases" "lion" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
The mouse likes the dog.
("mouse" "likes" "dog" "+")
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
If the lion needs the mouse then the lion likes the mouse.
((("lion" "needs" "mouse" "+")) -> ("lion" "likes" "mouse" "+"))
If the dog is blue then the dog likes the mouse.
((("dog" "is" "blue" "+")) -> ("dog" "likes" "mouse" "+"))
If the lion does not like the dog and the dog does not need the mouse then the dog does not need the lion.
((("lion" "likes" "dog" "~") ("dog" "needs" "mouse" "~")) -> ("dog" "needs" "lion" "-"))
If something is cold then it chases the dog.
((("something" "is" "cold" "+")) -> ("something" "chases" "dog" "+"))
If something is kind and it chases the lion then it chases the dog.
((("something" "is" "kind" "+") ("something" "chases" "lion" "+")) -> ("something" "chases" "dog" "+"))
If something is cold then it needs the dog.
((("something" "is" "cold" "+")) -> ("something" "needs" "dog" "+"))
If something needs the mouse and the mouse chases the lion then it is blue.
((("something" "needs" "mouse" "+") ("mouse" "chases" "lion" "+")) -> ("something" "is" "blue" "+"))
If something likes the mouse then it chases the lion.
((("something" "likes" "mouse" "+")) -> ("something" "chases" "lion" "+"))
The dog needs the mouse.
True
1
proof
[(triple3)]
("dog" "needs" "mouse" "+")
triple3
The mouse needs the lion.
False
1
inv-proof
[(triple10)]
("mouse" "needs" "lion" "+")
triple10
The mouse chases the dog.
True
3
proof
[(((triple8 triple7) -> rule5))]
("mouse" "chases" "dog" "+")
((triple8 triple7) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The mouse does not chase the dog.
False
3
inv-proof
[(((triple8 triple7) -> rule5))]
("mouse" "chases" "dog" "-")
((triple8 triple7) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog likes the mouse.
True
4
proof
[(((((triple3 triple7) -> rule7)) -> rule2))]
("dog" "likes" "mouse" "+")
((((triple3 triple7) -> (rule7 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog does not like the mouse.
False
4
inv-proof
[(((((triple3 triple7) -> rule7)) -> rule2))]
("dog" "likes" "mouse" "-")
((((triple3 triple7) -> (rule7 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog chases the lion.
True
5
proof
[(((((((triple3 triple7) -> rule7)) -> rule2)) -> rule8))]
("dog" "chases" "lion" "+")
((((((triple3 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The dog does not chase the lion.
False
5
inv-proof
[(((((((triple3 triple7) -> rule7)) -> rule2)) -> rule8))]
("dog" "chases" "lion" "-")
((((((triple3 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The mouse does not need the dog.
Unknown
inv-rconc
[@1: The mouse needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "needs" "dog" "-")
The dog needs the dog.
Unknown
rconc
[@1: The dog needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "needs" "dog" "+")
The lion is not blue.
Unknown
inv-rconc
[@1: The lion is blue.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "is" "blue" "-")
The lion needs the dog.
Unknown
rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "needs" "dog" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
The lion is not cold.
Unknown
inv-random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "-")
The lion is round.
Unknown
random
[@0: The lion is round.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "round" "+")
@0: The dog chases the mouse.[(triple1)] The dog needs the lion.[(triple2)] The dog needs the mouse.[(triple3)] The lion chases the dog.[(triple4)] The lion likes the dog.[(triple5)] The lion likes the mouse.[(triple6)] The mouse chases the lion.[(triple7)] The mouse does not need the lion.[(triple10)] The mouse is kind.[(triple8)] The mouse likes the dog.[(triple9)] @1: The dog is blue.[(((triple3 triple7) -> rule7))] The lion chases the lion.[(((triple6) -> rule8))] The mouse chases the dog.[(((triple8 triple7) -> rule5))] @2: The dog likes the mouse.[(((((triple3 triple7) -> rule7)) -> rule2))] @3: The dog chases the lion.[(((((((triple3 triple7) -> rule7)) -> rule2)) -> rule8))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog needs the lion.
("dog" "needs" "lion" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The lion chases the dog.
("lion" "chases" "dog" "+")
triple4
The lion likes the dog.
("lion" "likes" "dog" "+")
triple5
The lion likes the mouse.
("lion" "likes" "mouse" "+")
triple6
The mouse chases the lion.
("mouse" "chases" "lion" "+")
triple7
The mouse does not need the lion.
("mouse" "needs" "lion" "-")
triple10
The mouse is kind.
("mouse" "is" "kind" "+")
triple8
The mouse likes the dog.
("mouse" "likes" "dog" "+")
triple9
The dog is blue.
("dog" "is" "blue" "+")
((triple3 triple7) -> (rule7 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple6) -> (rule8 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((triple8 triple7) -> (rule5 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
((((triple3 triple7) -> (rule7 % int2))) -> (rule2 % int1))
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The dog chases the lion.
("dog" "chases" "lion" "+")
((((((triple3 triple7) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
The dog chases the lion.
("dog" "chases" "lion" "+")
int1
The dog likes the mouse.
("dog" "likes" "mouse" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3