The cat chases the lion. The cat eats the rabbit. The cat is green. The dog chases the lion. The dog eats the rabbit. The dog is blue. The dog is green. The lion eats the cat. The lion eats the dog. The rabbit chases the lion. The rabbit is young. The rabbit sees the cat. Green people are big. If someone sees the dog then the dog sees the lion. If someone is green and young then they chase the dog. If someone eats the cat and they are green then the cat eats the rabbit. If someone is big and they chase the dog then they eat the lion. Young people are green.
The cat chases the lion.
("cat" "chases" "lion" "+")
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
The cat is green.
("cat" "is" "green" "+")
The dog chases the lion.
("dog" "chases" "lion" "+")
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog is green.
("dog" "is" "green" "+")
The lion eats the cat.
("lion" "eats" "cat" "+")
The lion eats the dog.
("lion" "eats" "dog" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
Green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
If someone sees the dog then the dog sees the lion.
((("someone" "sees" "dog" "+")) -> ("dog" "sees" "lion" "+"))
If someone is green and young then they chase the dog.
((("someone" "is" "green" "+") ("someone" "is" "young" "+")) -> ("someone" "chases" "dog" "+"))
If someone eats the cat and they are green then the cat eats the rabbit.
((("someone" "eats" "cat" "+") ("someone" "is" "green" "+")) -> ("cat" "eats" "rabbit" "+"))
If someone is big and they chase the dog then they eat the lion.
((("someone" "is" "big" "+") ("someone" "chases" "dog" "+")) -> ("someone" "eats" "lion" "+"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
The rabbit is young.
True
1
proof
[(triple11)]
("rabbit" "is" "young" "+")
triple11
The dog does not eat the rabbit.
False
1
inv-proof
[(triple5)]
("dog" "eats" "rabbit" "-")
triple5
The dog is big.
True
2
proof
[(((triple7) -> rule1))]
("dog" "is" "big" "+")
((triple7) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The cat is not big.
False
2
inv-proof
[(((triple3) -> rule1))]
("cat" "is" "big" "-")
((triple3) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The rabbit is big.
True
3
proof
[(((((triple11) -> rule6)) -> rule1))]
("rabbit" "is" "big" "+")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is not big.
False
3
inv-proof
[(((((triple11) -> rule6)) -> rule1))]
("rabbit" "is" "big" "-")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit eats the lion.
True
8
proof
[(((((((triple11) -> rule6)) -> rule1) ((((triple11) -> rule6) triple11) -> rule3)) -> rule5))]
("rabbit" "eats" "lion" "+")
((((((triple11) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple11) -> (rule6 % int4)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The rabbit does not eat the lion.
False
8
inv-proof
[(((((((triple11) -> rule6)) -> rule1) ((((triple11) -> rule6) triple11) -> rule3)) -> rule5))]
("rabbit" "eats" "lion" "-")
((((((triple11) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple11) -> (rule6 % int4)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "is" "green" "-")
The cat eats the lion.
Unknown
rconc
[@2: The cat eats the lion.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("cat" "eats" "lion" "+")
The lion does not chase the dog.
Unknown
inv-rconc
[@1: The lion chases the dog.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("lion" "chases" "dog" "-")
The dog eats the lion.
Unknown
rconc
[@2: The dog eats the lion.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("dog" "eats" "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 rabbit eats the dog.
Unknown
random
[@0: The rabbit eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "dog" "+")
The cat does not eat the dog.
Unknown
inv-random
[@0: The cat eats the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "eats" "dog" "-")
The dog sees the cat.
Unknown
random
[@0: The dog sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cat" "+")
@0: The cat chases the lion.[(triple1)] The cat eats the rabbit.[(triple2)] The cat is green.[(triple3)] The dog chases the lion.[(triple4)] The dog eats the rabbit.[(triple5)] The dog is blue.[(triple6)] The dog is green.[(triple7)] The lion eats the cat.[(triple8)] The lion eats the dog.[(triple9)] The rabbit chases the lion.[(triple10)] The rabbit is young.[(triple11)] The rabbit sees the cat.[(triple12)] @1: The cat is big.[(((triple3) -> rule1))] The dog is big.[(((triple7) -> rule1))] The rabbit is green.[(((triple11) -> rule6))] @2: The rabbit chases the dog.[(((((triple11) -> rule6) triple11) -> rule3))] The rabbit is big.[(((((triple11) -> rule6)) -> rule1))] @3: The rabbit eats the lion.[(((((((triple11) -> rule6)) -> rule1) ((((triple11) -> rule6) triple11) -> rule3)) -> rule5))]
The cat chases the lion.
("cat" "chases" "lion" "+")
triple1
The cat eats the rabbit.
("cat" "eats" "rabbit" "+")
triple2
The cat is green.
("cat" "is" "green" "+")
triple3
The dog chases the lion.
("dog" "chases" "lion" "+")
triple4
The dog eats the rabbit.
("dog" "eats" "rabbit" "+")
triple5
The dog is blue.
("dog" "is" "blue" "+")
triple6
The dog is green.
("dog" "is" "green" "+")
triple7
The lion eats the cat.
("lion" "eats" "cat" "+")
triple8
The lion eats the dog.
("lion" "eats" "dog" "+")
triple9
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple10
The rabbit is young.
("rabbit" "is" "young" "+")
triple11
The rabbit sees the cat.
("rabbit" "sees" "cat" "+")
triple12
The cat is big.
("cat" "is" "big" "+")
((triple3) -> (rule1 % int1))
The cat is big.
("cat" "is" "big" "+")
int1
The dog is big.
("dog" "is" "big" "+")
((triple7) -> (rule1 % int1))
The dog is big.
("dog" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
((triple11) -> (rule6 % int1))
The rabbit is green.
("rabbit" "is" "green" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
((((triple11) -> (rule6 % int2)) triple11) -> (rule3 % int1))
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
((((triple11) -> (rule6 % int2))) -> (rule1 % int1))
The rabbit is big.
("rabbit" "is" "big" "+")
int1
The rabbit is green.
("rabbit" "is" "green" "+")
int2
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
((((((triple11) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple11) -> (rule6 % int4)) triple11) -> (rule3 % int2))) -> (rule5 % int1))
The rabbit eats the lion.
("rabbit" "eats" "lion" "+")
int1
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
int2
The rabbit is big.
("rabbit" "is" "big" "+")
int3
The rabbit is green.
("rabbit" "is" "green" "+")
int4