The cat chases the dog. The cat sees the dog. The dog is rough. The dog needs the cat. The lion chases the cat. The mouse needs the dog. The mouse sees the cat. If something is cold then it sees the mouse. If something is rough and it needs the cat then the cat chases the mouse. If the dog needs the cat and the dog sees the cat then the cat sees the lion. If something needs the cat then the cat needs the lion. If something sees the cat and it is cold then it sees the dog. If something is kind and it needs the mouse then the mouse is kind. If something needs the mouse then the mouse is rough. If something chases the dog and it chases the mouse then the mouse is cold.
The cat chases the dog.
("cat" "chases" "dog" "+")
The cat sees the dog.
("cat" "sees" "dog" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the cat.
("dog" "needs" "cat" "+")
The lion chases the cat.
("lion" "chases" "cat" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
If something is cold then it sees the mouse.
((("something" "is" "cold" "+")) -> ("something" "sees" "mouse" "+"))
If something is rough and it needs the cat then the cat chases the mouse.
((("something" "is" "rough" "+") ("something" "needs" "cat" "+")) -> ("cat" "chases" "mouse" "+"))
If the dog needs the cat and the dog sees the cat then the cat sees the lion.
((("dog" "needs" "cat" "+") ("dog" "sees" "cat" "+")) -> ("cat" "sees" "lion" "+"))
If something needs the cat then the cat needs the lion.
((("something" "needs" "cat" "+")) -> ("cat" "needs" "lion" "+"))
If something sees the cat and it is cold then it sees the dog.
((("something" "sees" "cat" "+") ("something" "is" "cold" "+")) -> ("something" "sees" "dog" "+"))
If something is kind and it needs the mouse then the mouse is kind.
((("something" "is" "kind" "+") ("something" "needs" "mouse" "+")) -> ("mouse" "is" "kind" "+"))
If something needs the mouse then the mouse is rough.
((("something" "needs" "mouse" "+")) -> ("mouse" "is" "rough" "+"))
If something chases the dog and it chases the mouse then the mouse is cold.
((("something" "chases" "dog" "+") ("something" "chases" "mouse" "+")) -> ("mouse" "is" "cold" "+"))
The cat chases the dog.
True
1
proof
[(triple1)]
("cat" "chases" "dog" "+")
triple1
The dog does not need the cat.
False
1
inv-proof
[(triple4)]
("dog" "needs" "cat" "-")
triple4
The cat needs the lion.
True
2
proof
[(((triple4) -> rule4))]
("cat" "needs" "lion" "+")
((triple4) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The cat does not need the lion.
False
2
inv-proof
[(((triple4) -> rule4))]
("cat" "needs" "lion" "-")
((triple4) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The mouse is cold.
True
5
proof
[(((triple1 ((triple3 triple4) -> rule2)) -> rule8))]
("mouse" "is" "cold" "+")
((triple1 ((triple3 triple4) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse is not cold.
False
5
inv-proof
[(((triple1 ((triple3 triple4) -> rule2)) -> rule8))]
("mouse" "is" "cold" "-")
((triple1 ((triple3 triple4) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse sees the dog.
True
7
proof
[(((triple7 ((triple1 ((triple3 triple4) -> rule2)) -> rule8)) -> rule5))]
("mouse" "sees" "dog" "+")
((triple7 ((triple1 ((triple3 triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse does not see the mouse.
False
6
inv-proof
[(((((triple1 ((triple3 triple4) -> rule2)) -> rule8)) -> rule1))]
("mouse" "sees" "mouse" "-")
((((triple1 ((triple3 triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The dog does not see the mouse.
Unknown
inv-rconc
[@1: The dog sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "sees" "mouse" "-")
The lion sees the mouse.
Unknown
rconc
[@1: The lion sees the mouse.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "sees" "mouse" "+")
The mouse is not kind.
Unknown
inv-rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "is" "kind" "-")
The lion sees the dog.
Unknown
rconc
[@1: The lion sees the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "sees" "dog" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The lion is cold.
Unknown
random
[@0: The lion is cold.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "cold" "+")
The mouse does not chase the cat.
Unknown
inv-random
[@0: The mouse chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "cat" "-")
The lion sees the lion.
Unknown
random
[@0: The lion sees the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "sees" "lion" "+")
@0: The cat chases the dog.[(triple1)] The cat sees the dog.[(triple2)] The dog is rough.[(triple3)] The dog needs the cat.[(triple4)] The lion chases the cat.[(triple5)] The mouse needs the dog.[(triple6)] The mouse sees the cat.[(triple7)] @1: The cat chases the mouse.[(((triple3 triple4) -> rule2))] The cat needs the lion.[(((triple4) -> rule4))] @2: The mouse is cold.[(((triple1 ((triple3 triple4) -> rule2)) -> rule8))] @3: The mouse sees the dog.[(((triple7 ((triple1 ((triple3 triple4) -> rule2)) -> rule8)) -> rule5))] The mouse sees the mouse.[(((((triple1 ((triple3 triple4) -> rule2)) -> rule8)) -> rule1))]
The cat chases the dog.
("cat" "chases" "dog" "+")
triple1
The cat sees the dog.
("cat" "sees" "dog" "+")
triple2
The dog is rough.
("dog" "is" "rough" "+")
triple3
The dog needs the cat.
("dog" "needs" "cat" "+")
triple4
The lion chases the cat.
("lion" "chases" "cat" "+")
triple5
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple6
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple7
The cat chases the mouse.
("cat" "chases" "mouse" "+")
((triple3 triple4) -> (rule2 % int1))
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int1
The cat needs the lion.
("cat" "needs" "lion" "+")
((triple4) -> (rule4 % int1))
The cat needs the lion.
("cat" "needs" "lion" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
((triple1 ((triple3 triple4) -> (rule2 % int2))) -> (rule8 % int1))
The mouse is cold.
("mouse" "is" "cold" "+")
int1
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int2
The mouse sees the dog.
("mouse" "sees" "dog" "+")
((triple7 ((triple1 ((triple3 triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule5 % int1))
The mouse sees the dog.
("mouse" "sees" "dog" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
((((triple1 ((triple3 triple4) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The mouse sees the mouse.
("mouse" "sees" "mouse" "+")
int1
The mouse is cold.
("mouse" "is" "cold" "+")
int2
The cat chases the mouse.
("cat" "chases" "mouse" "+")
int3