The bear chases the dog. The bear chases the lion. The bear chases the rabbit. The bear is red. The bear does not see the rabbit. The bear does not visit the lion. The dog does not chase the bear. The dog sees the bear. The dog visits the bear. The lion chases the rabbit. The lion visits the bear. The lion does not visit the dog. The lion does not visit the rabbit. The rabbit is nice. The rabbit sees the dog. The rabbit sees the lion. If something is red and it does not chase the dog then the dog does not see the rabbit. Big things are round. If something sees the rabbit then it is big. If something sees the bear then it sees the rabbit. If something chases the lion and the lion is not red then it visits the dog. If the rabbit is red and the rabbit visits the bear then the rabbit is not kind. If something visits the dog then it sees the lion. If the rabbit sees the dog and the rabbit does not see the bear then the rabbit sees the lion.
The bear chases the dog.
("bear" "chases" "dog" "+")
The bear chases the lion.
("bear" "chases" "lion" "+")
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is red.
("bear" "is" "red" "+")
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
The bear does not visit the lion.
("bear" "visits" "lion" "-")
The dog does not chase the bear.
("dog" "chases" "bear" "-")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog visits the bear.
("dog" "visits" "bear" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion visits the bear.
("lion" "visits" "bear" "+")
The lion does not visit the dog.
("lion" "visits" "dog" "-")
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If something is red and it does not chase the dog then the dog does not see the rabbit.
((("something" "is" "red" "+") ("something" "chases" "dog" "~")) -> ("dog" "sees" "rabbit" "-"))
Big things are round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
If something sees the rabbit then it is big.
((("something" "sees" "rabbit" "+")) -> ("something" "is" "big" "+"))
If something sees the bear then it sees the rabbit.
((("something" "sees" "bear" "+")) -> ("something" "sees" "rabbit" "+"))
If something chases the lion and the lion is not red then it visits the dog.
((("something" "chases" "lion" "+") ("lion" "is" "red" "~")) -> ("something" "visits" "dog" "+"))
If the rabbit is red and the rabbit visits the bear then the rabbit is not kind.
((("rabbit" "is" "red" "+") ("rabbit" "visits" "bear" "+")) -> ("rabbit" "is" "kind" "-"))
If something visits the dog then it sees the lion.
((("something" "visits" "dog" "+")) -> ("something" "sees" "lion" "+"))
If the rabbit sees the dog and the rabbit does not see the bear then the rabbit sees the lion.
((("rabbit" "sees" "dog" "+") ("rabbit" "sees" "bear" "~")) -> ("rabbit" "sees" "lion" "+"))
The dog sees the bear.
True
1
proof
[(triple8)]
("dog" "sees" "bear" "+")
triple8
The lion does not chase the rabbit.
False
1
inv-proof
[(triple10)]
("lion" "chases" "rabbit" "-")
triple10
The dog sees the rabbit.
True
2
proof
[(((triple8) -> rule4))]
("dog" "sees" "rabbit" "+")
((triple8) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog does not see the rabbit.
False
2
inv-proof
[(((triple8) -> rule4))]
("dog" "sees" "rabbit" "-")
((triple8) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog is big.
True
3
proof
[(((((triple8) -> rule4)) -> rule3))]
("dog" "is" "big" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog is not big.
False
3
inv-proof
[(((((triple8) -> rule4)) -> rule3))]
("dog" "is" "big" "-")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog is round.
True
4
proof
[(((((((triple8) -> rule4)) -> rule3)) -> rule2))]
("dog" "is" "round" "+")
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The dog is not round.
False
4
inv-proof
[(((((((triple8) -> rule4)) -> rule3)) -> rule2))]
("dog" "is" "round" "-")
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "big" "-")
The bear is round.
Unknown
rconc
[@2: The bear is round.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("bear" "is" "round" "+")
The rabbit is not big.
Unknown
inv-rconc
[@2: The rabbit is big.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "is" "big" "-")
The bear sees the lion.
Unknown
rconc
[@2: The bear sees the lion.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("bear" "sees" "lion" "+")
The dog does not see the dog.
Unknown
inv-random
[@0: The dog sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "dog" "-")
The dog chases the dog.
Unknown
random
[@0: The dog chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "chases" "dog" "+")
The bear does not visit the rabbit.
Unknown
inv-random
[@0: The bear visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "rabbit" "-")
The rabbit visits the bear.
Unknown
random
[@0: The rabbit visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "bear" "+")
@0: The bear chases the dog.[(triple1)] The bear chases the lion.[(triple2)] The bear chases the rabbit.[(triple3)] The bear does not see the rabbit.[(triple5)] The bear does not visit the lion.[(triple6)] The bear is red.[(triple4)] The dog does not chase the bear.[(triple7)] The dog sees the bear.[(triple8)] The dog visits the bear.[(triple9)] The lion chases the rabbit.[(triple10)] The lion does not visit the dog.[(triple12)] The lion does not visit the rabbit.[(triple13)] The lion visits the bear.[(triple11)] The rabbit is nice.[(triple14)] The rabbit sees the dog.[(triple15)] The rabbit sees the lion.[(triple16)] @1: The dog sees the rabbit.[(((triple8) -> rule4))] @2: The dog is big.[(((((triple8) -> rule4)) -> rule3))] @3: The dog is round.[(((((((triple8) -> rule4)) -> rule3)) -> rule2))]
The bear chases the dog.
("bear" "chases" "dog" "+")
triple1
The bear chases the lion.
("bear" "chases" "lion" "+")
triple2
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple3
The bear does not see the rabbit.
("bear" "sees" "rabbit" "-")
triple5
The bear does not visit the lion.
("bear" "visits" "lion" "-")
triple6
The bear is red.
("bear" "is" "red" "+")
triple4
The dog does not chase the bear.
("dog" "chases" "bear" "-")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
triple8
The dog visits the bear.
("dog" "visits" "bear" "+")
triple9
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple10
The lion does not visit the dog.
("lion" "visits" "dog" "-")
triple12
The lion does not visit the rabbit.
("lion" "visits" "rabbit" "-")
triple13
The lion visits the bear.
("lion" "visits" "bear" "+")
triple11
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple14
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
triple15
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple16
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((triple8) -> (rule4 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((((triple8) -> (rule4 % int2))) -> (rule3 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog is round.
("dog" "is" "round" "+")
((((((triple8) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog is round.
("dog" "is" "round" "+")
int1
The dog is big.
("dog" "is" "big" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3