The cat chases the mouse. The dog eats the lion. The lion is nice. The mouse eats the dog. If something is kind then it chases the cat. If the lion sees the cat then the cat sees the dog. If something chases the mouse and it sees the lion then it chases the lion. If something is nice and it chases the cat then it sees the dog. If something eats the dog then it chases the cat. If something eats the lion then the lion chases the cat.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The dog eats the lion.
("dog" "eats" "lion" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse eats the dog.
("mouse" "eats" "dog" "+")
If something is kind then it chases the cat.
((("something" "is" "kind" "+")) -> ("something" "chases" "cat" "+"))
If the lion sees the cat then the cat sees the dog.
((("lion" "sees" "cat" "+")) -> ("cat" "sees" "dog" "+"))
If something chases the mouse and it sees the lion then it chases the lion.
((("something" "chases" "mouse" "+") ("something" "sees" "lion" "+")) -> ("something" "chases" "lion" "+"))
If something is nice and it chases the cat then it sees the dog.
((("something" "is" "nice" "+") ("something" "chases" "cat" "+")) -> ("something" "sees" "dog" "+"))
If something eats the dog then it chases the cat.
((("something" "eats" "dog" "+")) -> ("something" "chases" "cat" "+"))
If something eats the lion then the lion chases the cat.
((("something" "eats" "lion" "+")) -> ("lion" "chases" "cat" "+"))
The dog eats the lion.
True
1
proof
[(triple2)]
("dog" "eats" "lion" "+")
triple2
The lion is not nice.
False
1
inv-proof
[(triple3)]
("lion" "is" "nice" "-")
triple3
The lion chases the cat.
True
2
proof
[(((triple2) -> rule6))]
("lion" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple2) -> rule6))]
("lion" "chases" "cat" "-")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion sees the dog.
True
4
proof
[(((triple3 ((triple2) -> rule6)) -> rule4))]
("lion" "sees" "dog" "+")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The lion does not see the dog.
False
4
inv-proof
[(((triple3 ((triple2) -> rule6)) -> rule4))]
("lion" "sees" "dog" "-")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The dog does not chase the lion.
Unknown
inv-rconc
[@1: The dog chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "lion" "-")
The mouse chases the lion.
Unknown
rconc
[@1: The mouse chases the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "chases" "lion" "+")
The mouse does not see the dog.
Unknown
inv-rconc
[@1: The mouse sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "sees" "dog" "-")
The dog is big.
Unknown
random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "+")
The dog is not nice.
Unknown
inv-random
[@0: The dog is nice.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "nice" "-")
The mouse chases the mouse.
Unknown
random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "+")
@0: The cat chases the mouse.[(triple1)] The dog eats the lion.[(triple2)] The lion is nice.[(triple3)] The mouse eats the dog.[(triple4)] @1: The lion chases the cat.[(((triple2) -> rule6))] The mouse chases the cat.[(((triple4) -> rule5))] @2: The lion sees the dog.[(((triple3 ((triple2) -> rule6)) -> rule4))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The dog eats the lion.
("dog" "eats" "lion" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The mouse eats the dog.
("mouse" "eats" "dog" "+")
triple4
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple2) -> (rule6 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The mouse chases the cat.
("mouse" "chases" "cat" "+")
((triple4) -> (rule5 % int1))
The mouse chases the cat.
("mouse" "chases" "cat" "+")
int1
The lion sees the dog.
("lion" "sees" "dog" "+")
((triple3 ((triple2) -> (rule6 % int2))) -> (rule4 % int1))
The lion sees the dog.
("lion" "sees" "dog" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2