The cow is red. The cow sees the lion. The dog eats the tiger. The dog is red. The dog is round. The dog sees the tiger. The dog visits the lion. The lion is not red. The lion sees the cow. The tiger is big. If someone eats the lion then the lion eats the tiger. If the lion visits the dog then the lion eats the dog. If someone sees the cow and they eat the lion then the lion visits the dog. If someone eats the tiger then they eat the lion. If someone is big then they do not see the cow.
The cow is red.
("cow" "is" "red" "+")
The cow sees the lion.
("cow" "sees" "lion" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is red.
("dog" "is" "red" "+")
The dog is round.
("dog" "is" "round" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The dog visits the lion.
("dog" "visits" "lion" "+")
The lion is not red.
("lion" "is" "red" "-")
The lion sees the cow.
("lion" "sees" "cow" "+")
The tiger is big.
("tiger" "is" "big" "+")
If someone eats the lion then the lion eats the tiger.
((("someone" "eats" "lion" "+")) -> ("lion" "eats" "tiger" "+"))
If the lion visits the dog then the lion eats the dog.
((("lion" "visits" "dog" "+")) -> ("lion" "eats" "dog" "+"))
If someone sees the cow and they eat the lion then the lion visits the dog.
((("someone" "sees" "cow" "+") ("someone" "eats" "lion" "+")) -> ("lion" "visits" "dog" "+"))
If someone eats the tiger then they eat the lion.
((("someone" "eats" "tiger" "+")) -> ("someone" "eats" "lion" "+"))
If someone is big then they do not see the cow.
((("someone" "is" "big" "+")) -> ("someone" "sees" "cow" "-"))
The lion is not red.
True
1
proof
[(triple8)]
("lion" "is" "red" "-")
triple8
The dog does not visit the lion.
False
1
inv-proof
[(triple7)]
("dog" "visits" "lion" "-")
triple7
The tiger does not see the cow.
True
2
proof
[(((triple10) -> rule5))]
("tiger" "sees" "cow" "-")
((triple10) -> (rule5 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The tiger sees the cow.
False
2
inv-proof
[(((triple10) -> rule5))]
("tiger" "sees" "cow" "+")
((triple10) -> (rule5 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The lion eats the tiger.
True
3
proof
[(((((triple3) -> rule4)) -> rule1))]
("lion" "eats" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
The lion does not eat the tiger.
False
3
inv-proof
[(((((triple3) -> rule4)) -> rule1))]
("lion" "eats" "tiger" "-")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
The lion eats the lion.
True
4
proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule4))]
("lion" "eats" "lion" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
int3
The lion does not eat the lion.
False
4
inv-proof
[(((((((triple3) -> rule4)) -> rule1)) -> rule4))]
("lion" "eats" "lion" "-")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
int3
The lion visits the dog.
True
6
proof
[(((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3))]
("lion" "visits" "dog" "+")
((triple9 ((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The dog eats the lion.
("dog" "eats" "lion" "+")
int4
The lion does not visit the dog.
False
6
inv-proof
[(((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3))]
("lion" "visits" "dog" "-")
((triple9 ((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The dog eats the lion.
("dog" "eats" "lion" "+")
int4
The lion eats the dog.
True
7
proof
[(((((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("lion" "eats" "dog" "+")
((((triple9 ((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int4
The dog eats the lion.
("dog" "eats" "lion" "+")
int5
The lion does not eat the dog.
False
7
inv-proof
[(((((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
("lion" "eats" "dog" "-")
((((triple9 ((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int4
The dog eats the lion.
("dog" "eats" "lion" "+")
int5
The cow does not eat the lion.
Unknown
inv-rconc
[@1: The cow eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cow" "eats" "lion" "-")
The tiger eats the lion.
Unknown
rconc
[@1: The tiger eats the lion.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "eats" "lion" "+")
The tiger does not eat the tiger.
Unknown
inv-random
[@0: The tiger eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "tiger" "-")
The dog is kind.
Unknown
random
[@0: The dog is kind.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "kind" "+")
The cow does not visit the tiger.
Unknown
inv-random
[@0: The cow visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "tiger" "-")
The tiger is kind.
Unknown
random
[@0: The tiger is kind.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "kind" "+")
The cow does not eat the dog.
Unknown
inv-random
[@0: The cow eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "eats" "dog" "-")
The lion visits the lion.
Unknown
random
[@0: The lion visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "lion" "+")
The tiger does not eat the dog.
Unknown
inv-random
[@0: The tiger eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "eats" "dog" "-")
The lion is kind.
Unknown
random
[@0: The lion is kind.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "kind" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The cow is red.[(triple1)] The cow sees the lion.[(triple2)] The dog eats the tiger.[(triple3)] The dog is red.[(triple4)] The dog is round.[(triple5)] The dog sees the tiger.[(triple6)] The dog visits the lion.[(triple7)] The lion is not red.[(triple8)] The lion sees the cow.[(triple9)] The tiger is big.[(triple10)] @1: The dog eats the lion.[(((triple3) -> rule4))] The tiger does not see the cow.[(((triple10) -> rule5))] @2: The lion eats the tiger.[(((((triple3) -> rule4)) -> rule1))] @3: The lion eats the lion.[(((((((triple3) -> rule4)) -> rule1)) -> rule4))] @4: The lion visits the dog.[(((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3))] @5: The lion eats the dog.[(((((triple9 ((((((triple3) -> rule4)) -> rule1)) -> rule4)) -> rule3)) -> rule2))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow sees the lion.
("cow" "sees" "lion" "+")
triple2
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple3
The dog is red.
("dog" "is" "red" "+")
triple4
The dog is round.
("dog" "is" "round" "+")
triple5
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple6
The dog visits the lion.
("dog" "visits" "lion" "+")
triple7
The lion is not red.
("lion" "is" "red" "-")
triple8
The lion sees the cow.
("lion" "sees" "cow" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The dog eats the lion.
("dog" "eats" "lion" "+")
((triple3) -> (rule4 % int1))
The dog eats the lion.
("dog" "eats" "lion" "+")
int1
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
((triple10) -> (rule5 % int1))
The tiger does not see the cow.
("tiger" "sees" "cow" "-")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
((((triple3) -> (rule4 % int2))) -> (rule1 % int1))
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int1
The dog eats the lion.
("dog" "eats" "lion" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
((((((triple3) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
The lion eats the lion.
("lion" "eats" "lion" "+")
int1
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int2
The dog eats the lion.
("dog" "eats" "lion" "+")
int3
The lion visits the dog.
("lion" "visits" "dog" "+")
((triple9 ((((((triple3) -> (rule4 % int4))) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The lion visits the dog.
("lion" "visits" "dog" "+")
int1
The lion eats the lion.
("lion" "eats" "lion" "+")
int2
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int3
The dog eats the lion.
("dog" "eats" "lion" "+")
int4
The lion eats the dog.
("lion" "eats" "dog" "+")
((((triple9 ((((((triple3) -> (rule4 % int5))) -> (rule1 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The lion eats the dog.
("lion" "eats" "dog" "+")
int1
The lion visits the dog.
("lion" "visits" "dog" "+")
int2
The lion eats the lion.
("lion" "eats" "lion" "+")
int3
The lion eats the tiger.
("lion" "eats" "tiger" "+")
int4
The dog eats the lion.
("dog" "eats" "lion" "+")
int5