The cat is cold. The cat needs the lion. The cat visits the rabbit. The dog visits the cat. The lion eats the cat. The lion needs the rabbit. The lion visits the cat. The lion visits the rabbit. The rabbit is nice. The rabbit needs the cat. The rabbit visits the lion. If someone visits the cat and the cat visits the rabbit then the rabbit needs the dog. If someone visits the cat and they are young then the cat is red. If someone is nice then they are cold. If someone eats the cat then they are young. If someone is nice then they need the dog. If the cat is red then the cat eats the lion. If the lion needs the rabbit and the rabbit eats the cat then the lion is cold. If someone eats the lion and they visit the lion then they need the dog. If someone eats the lion then they visit the lion.
The cat is cold.
("cat" "is" "cold" "+")
The cat needs the lion.
("cat" "needs" "lion" "+")
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
The dog visits the cat.
("dog" "visits" "cat" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The lion visits the cat.
("lion" "visits" "cat" "+")
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
If someone visits the cat and the cat visits the rabbit then the rabbit needs the dog.
((("someone" "visits" "cat" "+") ("cat" "visits" "rabbit" "+")) -> ("rabbit" "needs" "dog" "+"))
If someone visits the cat and they are young then the cat is red.
((("someone" "visits" "cat" "+") ("someone" "is" "young" "+")) -> ("cat" "is" "red" "+"))
If someone is nice then they are cold.
((("someone" "is" "nice" "+")) -> ("someone" "is" "cold" "+"))
If someone eats the cat then they are young.
((("someone" "eats" "cat" "+")) -> ("someone" "is" "young" "+"))
If someone is nice then they need the dog.
((("someone" "is" "nice" "+")) -> ("someone" "needs" "dog" "+"))
If the cat is red then the cat eats the lion.
((("cat" "is" "red" "+")) -> ("cat" "eats" "lion" "+"))
If the lion needs the rabbit and the rabbit eats the cat then the lion is cold.
((("lion" "needs" "rabbit" "+") ("rabbit" "eats" "cat" "+")) -> ("lion" "is" "cold" "+"))
If someone eats the lion and they visit the lion then they need the dog.
((("someone" "eats" "lion" "+") ("someone" "visits" "lion" "+")) -> ("someone" "needs" "dog" "+"))
If someone eats the lion then they visit the lion.
((("someone" "eats" "lion" "+")) -> ("someone" "visits" "lion" "+"))
The lion visits the cat.
True
1
proof
[(triple7)]
("lion" "visits" "cat" "+")
triple7
The cat does not need the lion.
False
1
inv-proof
[(triple2)]
("cat" "needs" "lion" "-")
triple2
The rabbit is cold.
True
2
proof
[(((triple9) -> rule3))]
("rabbit" "is" "cold" "+")
((triple9) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The lion is not young.
False
2
inv-proof
[(((triple5) -> rule4))]
("lion" "is" "young" "-")
((triple5) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The cat is red.
True
4
proof
[(((triple7 ((triple5) -> rule4)) -> rule2))]
("cat" "is" "red" "+")
((triple7 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cat is not red.
False
4
inv-proof
[(((triple7 ((triple5) -> rule4)) -> rule2))]
("cat" "is" "red" "-")
((triple7 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cat eats the lion.
True
5
proof
[(((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6))]
("cat" "eats" "lion" "+")
((((triple7 ((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The cat does not eat the lion.
False
5
inv-proof
[(((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6))]
("cat" "eats" "lion" "-")
((((triple7 ((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The cat visits the lion.
True
6
proof
[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9))]
("cat" "visits" "lion" "+")
((((((triple7 ((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The cat does not visit the lion.
False
6
inv-proof
[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9))]
("cat" "visits" "lion" "-")
((((((triple7 ((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The cat needs the dog.
True
12
proof
[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6) ((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9)) -> rule8))]
("cat" "needs" "dog" "+")
((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The cat does not need the dog.
False
12
inv-proof
[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6) ((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9)) -> rule8))]
("cat" "needs" "dog" "-")
((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5
The dog is not young.
Unknown
inv-rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "young" "-")
The cat is young.
Unknown
rconc
[@1: The cat is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "is" "young" "+")
The lion does not need the dog.
Unknown
inv-rconc
[@1: The lion needs the dog.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("lion" "needs" "dog" "-")
The rabbit is young.
Unknown
rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "is" "young" "+")
The lion does not visit the lion.
Unknown
inv-rconc
[@1: The lion visits the lion.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "visits" "lion" "-")
The lion is cold.
Unknown
rconc
[@1: The lion is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "is" "cold" "+")
The rabbit does not visit the dog.
Unknown
inv-random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "-")
The cat eats the cat.
Unknown
random
[@0: The cat eats the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "cat" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The cat is nice.
Unknown
random
[@0: The cat is nice.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "nice" "+")
The lion does not eat the lion.
Unknown
inv-random
[@0: The lion eats the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "eats" "lion" "-")
The cat eats the dog.
Unknown
random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "+")
@0: The cat is cold.[(triple1)] The cat needs the lion.[(triple2)] The cat visits the rabbit.[(triple3)] The dog visits the cat.[(triple4)] The lion eats the cat.[(triple5)] The lion needs the rabbit.[(triple6)] The lion visits the cat.[(triple7)] The lion visits the rabbit.[(triple8)] The rabbit is nice.[(triple9)] The rabbit needs the cat.[(triple10)] The rabbit visits the lion.[(triple11)] @1: The lion is young.[(((triple5) -> rule4))] The rabbit is cold.[(((triple9) -> rule3))] The rabbit needs the dog.[(((triple9) -> rule5) OR ((triple4 triple3) -> rule1) OR ((triple7 triple3) -> rule1))] @2: The cat is red.[(((triple7 ((triple5) -> rule4)) -> rule2))] @3: The cat eats the lion.[(((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6))] @4: The cat visits the lion.[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9))] @5: The cat needs the dog.[(((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6) ((((((triple7 ((triple5) -> rule4)) -> rule2)) -> rule6)) -> rule9)) -> rule8))]
The cat is cold.
("cat" "is" "cold" "+")
triple1
The cat needs the lion.
("cat" "needs" "lion" "+")
triple2
The cat visits the rabbit.
("cat" "visits" "rabbit" "+")
triple3
The dog visits the cat.
("dog" "visits" "cat" "+")
triple4
The lion eats the cat.
("lion" "eats" "cat" "+")
triple5
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple6
The lion visits the cat.
("lion" "visits" "cat" "+")
triple7
The lion visits the rabbit.
("lion" "visits" "rabbit" "+")
triple8
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple9
The rabbit needs the cat.
("rabbit" "needs" "cat" "+")
triple10
The rabbit visits the lion.
("rabbit" "visits" "lion" "+")
triple11
The lion is young.
("lion" "is" "young" "+")
((triple5) -> (rule4 % int1))
The lion is young.
("lion" "is" "young" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((triple9) -> (rule3 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((triple9) -> (rule5 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((triple4 triple3) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
((triple7 triple3) -> (rule1 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The cat is red.
("cat" "is" "red" "+")
((triple7 ((triple5) -> (rule4 % int2))) -> (rule2 % int1))
The cat is red.
("cat" "is" "red" "+")
int1
The lion is young.
("lion" "is" "young" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
((((triple7 ((triple5) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The cat eats the lion.
("cat" "eats" "lion" "+")
int1
The cat is red.
("cat" "is" "red" "+")
int2
The lion is young.
("lion" "is" "young" "+")
int3
The cat visits the lion.
("cat" "visits" "lion" "+")
((((((triple7 ((triple5) -> (rule4 % int4))) -> (rule2 % int3))) -> (rule6 % int2))) -> (rule9 % int1))
The cat visits the lion.
("cat" "visits" "lion" "+")
int1
The cat eats the lion.
("cat" "eats" "lion" "+")
int2
The cat is red.
("cat" "is" "red" "+")
int3
The lion is young.
("lion" "is" "young" "+")
int4
The cat needs the dog.
("cat" "needs" "dog" "+")
((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3)) ((((((triple7 ((triple5) -> (rule4 % int5))) -> (rule2 % int4))) -> (rule6 % int3))) -> (rule9 % int2))) -> (rule8 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The cat visits the lion.
("cat" "visits" "lion" "+")
int2
The cat eats the lion.
("cat" "eats" "lion" "+")
int3
The cat is red.
("cat" "is" "red" "+")
int4
The lion is young.
("lion" "is" "young" "+")
int5