The cat is red. The cat likes the lion. The cat does not need the rabbit. The cat sees the rabbit. The dog likes the rabbit. The lion is blue. The lion is not young. The rabbit is not nice. The rabbit likes the dog. The rabbit does not like the lion. If the rabbit sees the cat then the cat does not like the dog. If something sees the cat then the cat is not blue. If something is young and it sees the rabbit then it does not see the cat. If something is blue then it sees the cat. If something is rough and it likes the lion then the lion does not need the cat. If something sees the cat then it needs the dog. If something sees the lion and the lion likes the rabbit then it sees the rabbit. If something needs the dog then the dog is blue.
The cat is red.
("cat" "is" "red" "+")
The cat likes the lion.
("cat" "likes" "lion" "+")
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is not young.
("lion" "is" "young" "-")
The rabbit is not nice.
("rabbit" "is" "nice" "-")
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
If the rabbit sees the cat then the cat does not like the dog.
((("rabbit" "sees" "cat" "+")) -> ("cat" "likes" "dog" "-"))
If something sees the cat then the cat is not blue.
((("something" "sees" "cat" "+")) -> ("cat" "is" "blue" "-"))
If something is young and it sees the rabbit then it does not see the cat.
((("something" "is" "young" "+") ("something" "sees" "rabbit" "+")) -> ("something" "sees" "cat" "-"))
If something is blue then it sees the cat.
((("something" "is" "blue" "+")) -> ("something" "sees" "cat" "+"))
If something is rough and it likes the lion then the lion does not need the cat.
((("something" "is" "rough" "+") ("something" "likes" "lion" "+")) -> ("lion" "needs" "cat" "-"))
If something sees the cat then it needs the dog.
((("something" "sees" "cat" "+")) -> ("something" "needs" "dog" "+"))
If something sees the lion and the lion likes the rabbit then it sees the rabbit.
((("something" "sees" "lion" "+") ("lion" "likes" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something needs the dog then the dog is blue.
((("something" "needs" "dog" "+")) -> ("dog" "is" "blue" "+"))
The rabbit does not like the lion.
True
1
proof
[(triple10)]
("rabbit" "likes" "lion" "-")
triple10
The lion is not blue.
False
1
inv-proof
[(triple6)]
("lion" "is" "blue" "-")
triple6
The lion sees the cat.
True
2
proof
[(((triple6) -> rule4))]
("lion" "sees" "cat" "+")
((triple6) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The lion does not see the cat.
False
2
inv-proof
[(((triple6) -> rule4))]
("lion" "sees" "cat" "-")
((triple6) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat is not blue.
True
3
proof
[(((((triple6) -> rule4)) -> rule2) OR ((((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4)) -> rule2))]
("cat" "is" "blue" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The lion does not need the dog.
False
3
inv-proof
[(((((triple6) -> rule4)) -> rule6))]
("lion" "needs" "dog" "-")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The dog is blue.
True
4
proof
[(((((((triple6) -> rule4)) -> rule6)) -> rule8))]
("dog" "is" "blue" "+")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The dog is not blue.
False
4
inv-proof
[(((((((triple6) -> rule4)) -> rule6)) -> rule8))]
("dog" "is" "blue" "-")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The dog sees the cat.
True
5
proof
[(((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4))]
("dog" "sees" "cat" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The dog does not see the cat.
False
5
inv-proof
[(((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4))]
("dog" "sees" "cat" "-")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The dog needs the dog.
True
6
proof
[(((((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4)) -> rule6))]
("dog" "needs" "dog" "+")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The dog does not need the dog.
False
6
inv-proof
[(((((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4)) -> rule6))]
("dog" "needs" "dog" "-")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The rabbit does not need the dog.
Unknown
inv-rconc
[@2: The rabbit needs the dog.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("rabbit" "needs" "dog" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The cat needs the dog.
Unknown
rconc
[@2: The cat needs the dog.[CWA. Example of deepest failure = (rule6 <- rule4 <- FAIL)]]
("cat" "needs" "dog" "+")
The dog does not see the rabbit.
Unknown
inv-rconc
[@1: The dog sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "sees" "rabbit" "-")
The lion sees the rabbit.
Unknown
rconc
[@1: The lion sees the rabbit.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("lion" "sees" "rabbit" "+")
The cat does not need the cat.
Unknown
inv-random
[@0: The cat needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "cat" "-")
The rabbit sees the dog.
Unknown
random
[@0: The rabbit sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "dog" "+")
The lion does not need the cat.
Unknown
inv-random
[@0: The lion needs the cat.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cat" "-")
The lion likes the rabbit.
Unknown
random
[@0: The lion likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "likes" "rabbit" "+")
The lion does not need the rabbit.
Unknown
inv-random
[@0: The lion needs the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
@0: The cat does not need the rabbit.[(triple3)] The cat is red.[(triple1)] The cat likes the lion.[(triple2)] The cat sees the rabbit.[(triple4)] The dog likes the rabbit.[(triple5)] The lion is blue.[(triple6)] The lion is not young.[(triple7)] The rabbit does not like the lion.[(triple10)] The rabbit is not nice.[(triple8)] The rabbit likes the dog.[(triple9)] @1: The lion sees the cat.[(((triple6) -> rule4))] @2: The cat is not blue.[(((((triple6) -> rule4)) -> rule2) OR ((((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4)) -> rule2))] The lion needs the dog.[(((((triple6) -> rule4)) -> rule6))] @3: The dog is blue.[(((((((triple6) -> rule4)) -> rule6)) -> rule8))] @4: The dog sees the cat.[(((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4))] @5: The dog needs the dog.[(((((((((((triple6) -> rule4)) -> rule6)) -> rule8)) -> rule4)) -> rule6))]
The cat does not need the rabbit.
("cat" "needs" "rabbit" "-")
triple3
The cat is red.
("cat" "is" "red" "+")
triple1
The cat likes the lion.
("cat" "likes" "lion" "+")
triple2
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple4
The dog likes the rabbit.
("dog" "likes" "rabbit" "+")
triple5
The lion is blue.
("lion" "is" "blue" "+")
triple6
The lion is not young.
("lion" "is" "young" "-")
triple7
The rabbit does not like the lion.
("rabbit" "likes" "lion" "-")
triple10
The rabbit is not nice.
("rabbit" "is" "nice" "-")
triple8
The rabbit likes the dog.
("rabbit" "likes" "dog" "+")
triple9
The lion sees the cat.
("lion" "sees" "cat" "+")
((triple6) -> (rule4 % int1))
The lion sees the cat.
("lion" "sees" "cat" "+")
int1
The cat is not blue.
("cat" "is" "blue" "-")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
The cat is not blue.
("cat" "is" "blue" "-")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5
The lion needs the dog.
("lion" "needs" "dog" "+")
((((triple6) -> (rule4 % int2))) -> (rule6 % int1))
The lion needs the dog.
("lion" "needs" "dog" "+")
int1
The lion sees the cat.
("lion" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
((((((triple6) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
The dog is blue.
("dog" "is" "blue" "+")
int1
The lion needs the dog.
("lion" "needs" "dog" "+")
int2
The lion sees the cat.
("lion" "sees" "cat" "+")
int3
The dog sees the cat.
("dog" "sees" "cat" "+")
((((((((triple6) -> (rule4 % int4))) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
The dog sees the cat.
("dog" "sees" "cat" "+")
int1
The dog is blue.
("dog" "is" "blue" "+")
int2
The lion needs the dog.
("lion" "needs" "dog" "+")
int3
The lion sees the cat.
("lion" "sees" "cat" "+")
int4
The dog needs the dog.
("dog" "needs" "dog" "+")
((((((((((triple6) -> (rule4 % int5))) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The dog needs the dog.
("dog" "needs" "dog" "+")
int1
The dog sees the cat.
("dog" "sees" "cat" "+")
int2
The dog is blue.
("dog" "is" "blue" "+")
int3
The lion needs the dog.
("lion" "needs" "dog" "+")
int4
The lion sees the cat.
("lion" "sees" "cat" "+")
int5