The bear is young. The bear sees the dog. The bear visits the rabbit. The cow is cold. The cow visits the dog. The dog does not eat the rabbit. The dog is blue. The dog is young. The rabbit visits the cow. The rabbit does not visit the dog. If the cow eats the bear and the cow is blue then the cow visits the dog. If something sees the cow and the cow sees the rabbit then it sees the rabbit. If something eats the bear then it sees the rabbit. If something sees the rabbit then the rabbit is red. If something visits the rabbit and the rabbit visits the dog then the rabbit eats the bear. All blue, cold things are round. If something visits the rabbit then the rabbit is round. If something is blue then it eats the bear. If something is red then it eats the bear.
The bear is young.
("bear" "is" "young" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
The dog is blue.
("dog" "is" "blue" "+")
The dog is young.
("dog" "is" "young" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
If the cow eats the bear and the cow is blue then the cow visits the dog.
((("cow" "eats" "bear" "+") ("cow" "is" "blue" "+")) -> ("cow" "visits" "dog" "+"))
If something sees the cow and the cow sees the rabbit then it sees the rabbit.
((("something" "sees" "cow" "+") ("cow" "sees" "rabbit" "+")) -> ("something" "sees" "rabbit" "+"))
If something eats the bear then it sees the rabbit.
((("something" "eats" "bear" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the rabbit then the rabbit is red.
((("something" "sees" "rabbit" "+")) -> ("rabbit" "is" "red" "+"))
If something visits the rabbit and the rabbit visits the dog then the rabbit eats the bear.
((("something" "visits" "rabbit" "+") ("rabbit" "visits" "dog" "+")) -> ("rabbit" "eats" "bear" "+"))
All blue, cold things are round.
((("something" "is" "blue" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
If something visits the rabbit then the rabbit is round.
((("something" "visits" "rabbit" "+")) -> ("rabbit" "is" "round" "+"))
If something is blue then it eats the bear.
((("something" "is" "blue" "+")) -> ("something" "eats" "bear" "+"))
If something is red then it eats the bear.
((("something" "is" "red" "+")) -> ("something" "eats" "bear" "+"))
The rabbit does not visit the dog.
True
1
proof
[(triple10)]
("rabbit" "visits" "dog" "-")
triple10
The dog is not young.
False
1
inv-proof
[(triple8)]
("dog" "is" "young" "-")
triple8
The dog eats the bear.
True
2
proof
[(((triple7) -> rule8))]
("dog" "eats" "bear" "+")
((triple7) -> (rule8 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The rabbit is not round.
False
2
inv-proof
[(((triple3) -> rule7))]
("rabbit" "is" "round" "-")
((triple3) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The dog sees the rabbit.
True
3
proof
[(((((triple7) -> rule8)) -> rule3))]
("dog" "sees" "rabbit" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The dog does not see the rabbit.
False
3
inv-proof
[(((((triple7) -> rule8)) -> rule3))]
("dog" "sees" "rabbit" "-")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The rabbit is red.
True
4
proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule4))]
("rabbit" "is" "red" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The rabbit is not red.
False
4
inv-proof
[(((((((triple7) -> rule8)) -> rule3)) -> rule4))]
("rabbit" "is" "red" "-")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The rabbit eats the bear.
True
5
proof
[(((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9))]
("rabbit" "eats" "bear" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The rabbit does not eat the bear.
False
5
inv-proof
[(((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9))]
("rabbit" "eats" "bear" "-")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The rabbit sees the rabbit.
True
6
proof
[(((((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9)) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog eats the bear.
("dog" "eats" "bear" "+")
int5
The rabbit does not see the rabbit.
False
6
inv-proof
[(((((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9)) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog eats the bear.
("dog" "eats" "bear" "+")
int5
The cow does not eat the bear.
Unknown
inv-rconc
[@1: The cow eats the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "eats" "bear" "-")
The cow sees the rabbit.
Unknown
rconc
[@2: The cow sees the rabbit.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("cow" "sees" "rabbit" "+")
The cow is not round.
Unknown
inv-rconc
[@1: The cow is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("cow" "is" "round" "-")
The bear is round.
Unknown
rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "+")
The bear does not see the rabbit.
Unknown
inv-rconc
[@2: The bear sees the rabbit.[CWA. Example of deepest failure = (rule3 <- rule8 <- FAIL)]]
("bear" "sees" "rabbit" "-")
The bear eats the bear.
Unknown
rconc
[@1: The bear eats the bear.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("bear" "eats" "bear" "+")
The cow is not red.
Unknown
inv-random
[@0: The cow is red.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "red" "-")
The dog visits the bear.
Unknown
random
[@0: The dog visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "bear" "+")
The cow does not visit the bear.
Unknown
inv-random
[@0: The cow visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "bear" "-")
The cow eats the cow.
Unknown
random
[@0: The cow eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "cow" "+")
The dog is not cold.
Unknown
inv-random
[@0: The dog is cold.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "cold" "-")
The bear sees the cow.
Unknown
random
[@0: The bear sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "cow" "+")
@0: The bear is young.[(triple1)] The bear sees the dog.[(triple2)] The bear visits the rabbit.[(triple3)] The cow is cold.[(triple4)] The cow visits the dog.[(triple5)] The dog does not eat the rabbit.[(triple6)] The dog is blue.[(triple7)] The dog is young.[(triple8)] The rabbit does not visit the dog.[(triple10)] The rabbit visits the cow.[(triple9)] @1: The dog eats the bear.[(((triple7) -> rule8))] The rabbit is round.[(((triple3) -> rule7))] @2: The dog sees the rabbit.[(((((triple7) -> rule8)) -> rule3))] @3: The rabbit is red.[(((((((triple7) -> rule8)) -> rule3)) -> rule4))] @4: The rabbit eats the bear.[(((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9))] @5: The rabbit sees the rabbit.[(((((((((((triple7) -> rule8)) -> rule3)) -> rule4)) -> rule9)) -> rule3))]
The bear is young.
("bear" "is" "young" "+")
triple1
The bear sees the dog.
("bear" "sees" "dog" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
The cow visits the dog.
("cow" "visits" "dog" "+")
triple5
The dog does not eat the rabbit.
("dog" "eats" "rabbit" "-")
triple6
The dog is blue.
("dog" "is" "blue" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
triple8
The rabbit does not visit the dog.
("rabbit" "visits" "dog" "-")
triple10
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple9
The dog eats the bear.
("dog" "eats" "bear" "+")
((triple7) -> (rule8 % int1))
The dog eats the bear.
("dog" "eats" "bear" "+")
int1
The rabbit is round.
("rabbit" "is" "round" "+")
((triple3) -> (rule7 % int1))
The rabbit is round.
("rabbit" "is" "round" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
((((triple7) -> (rule8 % int2))) -> (rule3 % int1))
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int1
The dog eats the bear.
("dog" "eats" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
((((((triple7) -> (rule8 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The rabbit is red.
("rabbit" "is" "red" "+")
int1
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int2
The dog eats the bear.
("dog" "eats" "bear" "+")
int3
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
((((((((triple7) -> (rule8 % int4))) -> (rule3 % int3))) -> (rule4 % int2))) -> (rule9 % int1))
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int1
The rabbit is red.
("rabbit" "is" "red" "+")
int2
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int3
The dog eats the bear.
("dog" "eats" "bear" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((((triple7) -> (rule8 % int5))) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule9 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit eats the bear.
("rabbit" "eats" "bear" "+")
int2
The rabbit is red.
("rabbit" "is" "red" "+")
int3
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
int4
The dog eats the bear.
("dog" "eats" "bear" "+")
int5