The cat is red. The dog is kind. The dog needs the lion. The dog visits the lion. The lion needs the dog. The rabbit is cold. The rabbit does not need the lion. The rabbit does not see the cat. The rabbit sees the dog. The rabbit sees the lion. If someone is cold then they visit the rabbit. If someone is red then they need the dog. If the rabbit sees the dog and the dog is cold then the dog does not visit the rabbit. If someone is round then they need the rabbit. If someone sees the rabbit and they do not see the dog then they need the rabbit. If someone needs the dog then they do not see the rabbit. If someone sees the lion then they are round. If someone needs the rabbit then the rabbit is red. If someone visits the lion and the lion does not visit the dog then the lion is round.
The cat is red.
("cat" "is" "red" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog needs the lion.
("dog" "needs" "lion" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone is cold then they visit the rabbit.
((("someone" "is" "cold" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone is red then they need the dog.
((("someone" "is" "red" "+")) -> ("someone" "needs" "dog" "+"))
If the rabbit sees the dog and the dog is cold then the dog does not visit the rabbit.
((("rabbit" "sees" "dog" "+") ("dog" "is" "cold" "+")) -> ("dog" "visits" "rabbit" "-"))
If someone is round then they need the rabbit.
((("someone" "is" "round" "+")) -> ("someone" "needs" "rabbit" "+"))
If someone sees the rabbit and they do not see the dog then they need the rabbit.
((("someone" "sees" "rabbit" "+") ("someone" "sees" "dog" "~")) -> ("someone" "needs" "rabbit" "+"))
If someone needs the dog then they do not see the rabbit.
((("someone" "needs" "dog" "+")) -> ("someone" "sees" "rabbit" "-"))
If someone sees the lion then they are round.
((("someone" "sees" "lion" "+")) -> ("someone" "is" "round" "+"))
If someone needs the rabbit then the rabbit is red.
((("someone" "needs" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If someone visits the lion and the lion does not visit the dog then the lion is round.
((("someone" "visits" "lion" "+") ("lion" "visits" "dog" "~")) -> ("lion" "is" "round" "+"))
The dog visits the lion.
True
1
proof
[(triple4)]
("dog" "visits" "lion" "+")
triple4
The rabbit is not cold.
False
1
inv-proof
[(triple6)]
("rabbit" "is" "cold" "-")
triple6
The rabbit visits the rabbit.
True
2
proof
[(((triple6) -> rule1))]
("rabbit" "visits" "rabbit" "+")
((triple6) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit does not visit the rabbit.
False
2
inv-proof
[(((triple6) -> rule1))]
("rabbit" "visits" "rabbit" "-")
((triple6) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat does not see the rabbit.
True
3
proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "sees" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The cat sees the rabbit.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule6))]
("cat" "sees" "rabbit" "+")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The rabbit is red.
True
4
proof
[(((((((triple10) -> rule7)) -> rule4)) -> rule8))]
("rabbit" "is" "red" "+")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit is not red.
False
4
inv-proof
[(((((((triple10) -> rule7)) -> rule4)) -> rule8))]
("rabbit" "is" "red" "-")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit needs the dog.
True
5
proof
[(((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2))]
("rabbit" "needs" "dog" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The rabbit does not need the dog.
False
5
inv-proof
[(((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2))]
("rabbit" "needs" "dog" "-")
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The rabbit does not see the rabbit.
True
6
proof
[(((((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2)) -> rule6))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple10) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5
The rabbit sees the rabbit.
False
6
inv-proof
[(((((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2)) -> rule6))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple10) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5
The dog does not need the rabbit.
Unknown
inv-rconc
[@2: The dog needs the rabbit.[CWA. Example of deepest failure = (rule4 <- rule7 <- FAIL)]]
("dog" "needs" "rabbit" "-")
The cat visits the rabbit.
Unknown
rconc
[@1: The cat visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "visits" "rabbit" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("dog" "is" "round" "-")
The lion visits the rabbit.
Unknown
rconc
[@1: The lion visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("lion" "visits" "rabbit" "+")
The dog does not visit the rabbit.
Unknown
inv-rconc
[@1: The dog visits the rabbit.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "visits" "rabbit" "-")
The cat is round.
Unknown
rconc
[@1: The cat is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cat" "is" "round" "+")
The lion does not visit the dog.
Unknown
inv-random
[@0: The lion visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "dog" "-")
The lion is red.
Unknown
random
[@0: The lion is red.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "red" "+")
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 dog sees the dog.
Unknown
random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "+")
The lion is not rough.
Unknown
inv-random
[@0: The lion is rough.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "rough" "-")
The cat needs the lion.
Unknown
random
[@0: The cat needs the lion.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "lion" "+")
@0: The cat is red.[(triple1)] The dog is kind.[(triple2)] The dog needs the lion.[(triple3)] The dog visits the lion.[(triple4)] The lion needs the dog.[(triple5)] The rabbit does not need the lion.[(triple7)] The rabbit does not see the cat.[(triple8)] The rabbit is cold.[(triple6)] The rabbit sees the dog.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The cat needs the dog.[(((triple1) -> rule2))] The lion does not see the rabbit.[(((triple5) -> rule6))] The rabbit is round.[(((triple10) -> rule7))] The rabbit visits the rabbit.[(((triple6) -> rule1))] @2: The cat does not see the rabbit.[(((((triple1) -> rule2)) -> rule6))] The rabbit needs the rabbit.[(((((triple10) -> rule7)) -> rule4))] @3: The rabbit is red.[(((((((triple10) -> rule7)) -> rule4)) -> rule8))] @4: The rabbit needs the dog.[(((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2))] @5: The rabbit does not see the rabbit.[(((((((((((triple10) -> rule7)) -> rule4)) -> rule8)) -> rule2)) -> rule6))]
The cat is red.
("cat" "is" "red" "+")
triple1
The dog is kind.
("dog" "is" "kind" "+")
triple2
The dog needs the lion.
("dog" "needs" "lion" "+")
triple3
The dog visits the lion.
("dog" "visits" "lion" "+")
triple4
The lion needs the dog.
("lion" "needs" "dog" "+")
triple5
The rabbit does not need the lion.
("rabbit" "needs" "lion" "-")
triple7
The rabbit does not see the cat.
("rabbit" "sees" "cat" "-")
triple8
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple6
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The cat needs the dog.
("cat" "needs" "dog" "+")
((triple1) -> (rule2 % int1))
The cat needs the dog.
("cat" "needs" "dog" "+")
int1
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
((triple5) -> (rule6 % int1))
The lion does not see the rabbit.
("lion" "sees" "rabbit" "-")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple10) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple6) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
((((triple1) -> (rule2 % int2))) -> (rule6 % int1))
The cat does not see the rabbit.
("cat" "sees" "rabbit" "-")
int1
The cat needs the dog.
("cat" "needs" "dog" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
((((triple10) -> (rule7 % int2))) -> (rule4 % int1))
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((((triple10) -> (rule7 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int2
The rabbit is round.
("rabbit" "is" "round" "+")
int3
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
((((((((triple10) -> (rule7 % int4))) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule2 % int1))
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int3
The rabbit is round.
("rabbit" "is" "round" "+")
int4
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
((((((((((triple10) -> (rule7 % int5))) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
The rabbit does not see the rabbit.
("rabbit" "sees" "rabbit" "-")
int1
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The rabbit needs the rabbit.
("rabbit" "needs" "rabbit" "+")
int4
The rabbit is round.
("rabbit" "is" "round" "+")
int5