The cat chases the dog. The cat chases the lion. The cat chases the mouse. The cat eats the dog. The cat is big. The dog eats the cat. The dog eats the mouse. The dog is green. The dog needs the lion. The lion chases the cat. The lion chases the dog. The lion is green. The lion is red. The mouse chases the cat. The mouse eats the cat. The mouse is kind. If the lion needs the dog and the dog chases the mouse then the lion is nice. If someone is kind then they are big. If someone is big then they need the dog.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat is big.
("cat" "is" "big" "+")
The dog eats the cat.
("dog" "eats" "cat" "+")
The dog eats the mouse.
("dog" "eats" "mouse" "+")
The dog is green.
("dog" "is" "green" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion is green.
("lion" "is" "green" "+")
The lion is red.
("lion" "is" "red" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse eats the cat.
("mouse" "eats" "cat" "+")
The mouse is kind.
("mouse" "is" "kind" "+")
If the lion needs the dog and the dog chases the mouse then the lion is nice.
((("lion" "needs" "dog" "+") ("dog" "chases" "mouse" "+")) -> ("lion" "is" "nice" "+"))
If someone is kind then they are big.
((("someone" "is" "kind" "+")) -> ("someone" "is" "big" "+"))
If someone is big then they need the dog.
((("someone" "is" "big" "+")) -> ("someone" "needs" "dog" "+"))
The lion chases the dog.
True
1
proof
[(triple11)]
("lion" "chases" "dog" "+")
triple11
The lion does not chase the cat.
False
1
inv-proof
[(triple10)]
("lion" "chases" "cat" "-")
triple10
The mouse is big.
True
2
proof
[(((triple16) -> rule2))]
("mouse" "is" "big" "+")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse is not big.
False
2
inv-proof
[(((triple16) -> rule2))]
("mouse" "is" "big" "-")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the dog.
True
3
proof
[(((((triple16) -> rule2)) -> rule3))]
("mouse" "needs" "dog" "+")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The mouse does not need the dog.
False
3
inv-proof
[(((((triple16) -> rule2)) -> rule3))]
("mouse" "needs" "dog" "-")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2
The lion is not big.
Unknown
inv-rconc
[@1: The lion is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "is" "big" "-")
The lion is nice.
Unknown
rconc
[@1: The lion is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "is" "nice" "+")
The dog is not big.
Unknown
inv-rconc
[@1: The dog is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "big" "-")
The lion eats the dog.
Unknown
random
[@0: The lion eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "dog" "+")
The cat is not red.
Unknown
inv-random
[@0: The cat is red.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "red" "-")
The mouse chases the lion.
Unknown
random
[@0: The mouse chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "lion" "+")
@0: The cat chases the dog.[(triple1)] The cat chases the lion.[(triple2)] The cat chases the mouse.[(triple3)] The cat eats the dog.[(triple4)] The cat is big.[(triple5)] The dog eats the cat.[(triple6)] The dog eats the mouse.[(triple7)] The dog is green.[(triple8)] The dog needs the lion.[(triple9)] The lion chases the cat.[(triple10)] The lion chases the dog.[(triple11)] The lion is green.[(triple12)] The lion is red.[(triple13)] The mouse chases the cat.[(triple14)] The mouse eats the cat.[(triple15)] The mouse is kind.[(triple16)] @1: The cat needs the dog.[(((triple5) -> rule3))] The mouse is big.[(((triple16) -> rule2))] @2: The mouse needs the dog.[(((((triple16) -> rule2)) -> rule3))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat chases the lion.
("cat" "chases" "lion" "+")
triple2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple3
The cat eats the dog.
("cat" "eats" "dog" "+")
triple4
The cat is big.
("cat" "is" "big" "+")
triple5
The dog eats the cat.
("dog" "eats" "cat" "+")
triple6
The dog eats the mouse.
("dog" "eats" "mouse" "+")
triple7
The dog is green.
("dog" "is" "green" "+")
triple8
The dog needs the lion.
("dog" "needs" "lion" "+")
triple9
The lion chases the cat.
("lion" "chases" "cat" "+")
triple10
The lion chases the dog.
("lion" "chases" "dog" "+")
triple11
The lion is green.
("lion" "is" "green" "+")
triple12
The lion is red.
("lion" "is" "red" "+")
triple13
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple14
The mouse eats the cat.
("mouse" "eats" "cat" "+")
triple15
The mouse is kind.
("mouse" "is" "kind" "+")
triple16
The cat needs the dog.
("cat" "needs" "dog" "+")
((triple5) -> (rule3 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
((triple16) -> (rule2 % int1))
The mouse is big.
("mouse" "is" "big" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
The mouse needs the dog.
("mouse" "needs" "dog" "+")
int1
The mouse is big.
("mouse" "is" "big" "+")
int2