The cat chases the lion. The cat is big. The cat is kind. The cat needs the dog. The dog does not chase the cat. The dog is cold. The dog sees the lion. The lion does not chase the dog. The lion needs the dog. The lion sees the cat. If someone needs the dog then they chase the cat. If the dog chases the lion and the dog sees the lion then the lion chases the dog. If someone is green then they see the lion. If someone sees the cat then they need the lion. If the lion sees the cat and the cat sees the dog then the dog is not kind. If someone needs the lion then the lion is green. If someone needs the cat then they need the dog. If someone is big and they see the dog then they are kind.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat is big.
("cat" "is" "big" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The dog is cold.
("dog" "is" "cold" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion does not chase the dog.
("lion" "chases" "dog" "-")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If someone needs the dog then they chase the cat.
((("someone" "needs" "dog" "+")) -> ("someone" "chases" "cat" "+"))
If the dog chases the lion and the dog sees the lion then the lion chases the dog.
((("dog" "chases" "lion" "+") ("dog" "sees" "lion" "+")) -> ("lion" "chases" "dog" "+"))
If someone is green then they see the lion.
((("someone" "is" "green" "+")) -> ("someone" "sees" "lion" "+"))
If someone sees the cat then they need the lion.
((("someone" "sees" "cat" "+")) -> ("someone" "needs" "lion" "+"))
If the lion sees the cat and the cat sees the dog then the dog is not kind.
((("lion" "sees" "cat" "+") ("cat" "sees" "dog" "+")) -> ("dog" "is" "kind" "-"))
If someone needs the lion then the lion is green.
((("someone" "needs" "lion" "+")) -> ("lion" "is" "green" "+"))
If someone needs the cat then they need the dog.
((("someone" "needs" "cat" "+")) -> ("someone" "needs" "dog" "+"))
If someone is big and they see the dog then they are kind.
((("someone" "is" "big" "+") ("someone" "sees" "dog" "+")) -> ("someone" "is" "kind" "+"))
The cat is big.
True
1
proof
[(triple2)]
("cat" "is" "big" "+")
triple2
The cat is not big.
False
1
inv-proof
[(triple2)]
("cat" "is" "big" "-")
triple2
The lion chases the cat.
True
2
proof
[(((triple9) -> rule1))]
("lion" "chases" "cat" "+")
((triple9) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion does not chase the cat.
False
2
inv-proof
[(((triple9) -> rule1))]
("lion" "chases" "cat" "-")
((triple9) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion is green.
True
3
proof
[(((((triple10) -> rule4)) -> rule6))]
("lion" "is" "green" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion is not green.
False
3
inv-proof
[(((((triple10) -> rule4)) -> rule6))]
("lion" "is" "green" "-")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion sees the lion.
True
4
proof
[(((((((triple10) -> rule4)) -> rule6)) -> rule3))]
("lion" "sees" "lion" "+")
((((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The lion does not see the lion.
False
4
inv-proof
[(((((((triple10) -> rule4)) -> rule6)) -> rule3))]
("lion" "sees" "lion" "-")
((((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3
The dog does not need the lion.
Unknown
inv-rconc
[@1: The dog needs the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "needs" "lion" "-")
The cat sees the lion.
Unknown
rconc
[@1: The cat sees the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "sees" "lion" "+")
The dog is not kind.
Unknown
inv-rconc
[@1: The dog is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("dog" "is" "kind" "-")
The lion is kind.
Unknown
rconc
[@1: The lion is kind.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("lion" "is" "kind" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog is rough.
Unknown
random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "+")
The lion does not chase the lion.
Unknown
inv-random
[@0: The lion chases the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "lion" "-")
The lion needs the cat.
Unknown
random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "+")
@0: The cat chases the lion.[(triple1)] The cat is big.[(triple2)] The cat is kind.[(triple3)] The cat needs the dog.[(triple4)] The dog does not chase the cat.[(triple5)] The dog is cold.[(triple6)] The dog sees the lion.[(triple7)] The lion does not chase the dog.[(triple8)] The lion needs the dog.[(triple9)] The lion sees the cat.[(triple10)] @1: The cat chases the cat.[(((triple4) -> rule1))] The lion chases the cat.[(((triple9) -> rule1))] The lion needs the lion.[(((triple10) -> rule4))] @2: The lion is green.[(((((triple10) -> rule4)) -> rule6))] @3: The lion sees the lion.[(((((((triple10) -> rule4)) -> rule6)) -> rule3))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat is big.
("cat" "is" "big" "+")
triple2
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cat needs the dog.
("cat" "needs" "dog" "+")
triple4
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple5
The dog is cold.
("dog" "is" "cold" "+")
triple6
The dog sees the lion.
("dog" "sees" "lion" "+")
triple7
The lion does not chase the dog.
("lion" "chases" "dog" "-")
triple8
The lion needs the dog.
("lion" "needs" "dog" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
triple10
The cat chases the cat.
("cat" "chases" "cat" "+")
((triple4) -> (rule1 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
((triple9) -> (rule1 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
((triple10) -> (rule4 % int1))
The lion needs the lion.
("lion" "needs" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((((triple10) -> (rule4 % int2))) -> (rule6 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion needs the lion.
("lion" "needs" "lion" "+")
int2
The lion sees the lion.
("lion" "sees" "lion" "+")
((((((triple10) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The lion sees the lion.
("lion" "sees" "lion" "+")
int1
The lion is green.
("lion" "is" "green" "+")
int2
The lion needs the lion.
("lion" "needs" "lion" "+")
int3