The cow is big. The dog visits the cow. The lion chases the dog. The lion chases the rabbit. The rabbit chases the lion. The rabbit sees the cow. The rabbit visits the cow. If something visits the cow and the cow sees the dog then the cow visits the dog. If something chases the cow then it is blue. If something is green then it sees the dog. If something is big then it is green. If something sees the lion and the lion visits the rabbit then the rabbit is young. If the rabbit visits the cow and the cow visits the dog then the rabbit chases the cow. If something chases the cow and it sees the lion then it chases the lion. If the rabbit sees the cow then the cow visits the rabbit.
The cow is big.
("cow" "is" "big" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The lion chases the dog.
("lion" "chases" "dog" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
If something visits the cow and the cow sees the dog then the cow visits the dog.
((("something" "visits" "cow" "+") ("cow" "sees" "dog" "+")) -> ("cow" "visits" "dog" "+"))
If something chases the cow then it is blue.
((("something" "chases" "cow" "+")) -> ("something" "is" "blue" "+"))
If something is green then it sees the dog.
((("something" "is" "green" "+")) -> ("something" "sees" "dog" "+"))
If something is big then it is green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something sees the lion and the lion visits the rabbit then the rabbit is young.
((("something" "sees" "lion" "+") ("lion" "visits" "rabbit" "+")) -> ("rabbit" "is" "young" "+"))
If the rabbit visits the cow and the cow visits the dog then the rabbit chases the cow.
((("rabbit" "visits" "cow" "+") ("cow" "visits" "dog" "+")) -> ("rabbit" "chases" "cow" "+"))
If something chases the cow and it sees the lion then it chases the lion.
((("something" "chases" "cow" "+") ("something" "sees" "lion" "+")) -> ("something" "chases" "lion" "+"))
If the rabbit sees the cow then the cow visits the rabbit.
((("rabbit" "sees" "cow" "+")) -> ("cow" "visits" "rabbit" "+"))
The cow is big.
True
1
proof
[(triple1)]
("cow" "is" "big" "+")
triple1
The lion does not chase the dog.
False
1
inv-proof
[(triple3)]
("lion" "chases" "dog" "-")
triple3
The cow visits the rabbit.
True
2
proof
[(((triple6) -> rule8))]
("cow" "visits" "rabbit" "+")
((triple6) -> (rule8 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The cow is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("cow" "is" "green" "-")
((triple1) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow sees the dog.
True
3
proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "sees" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow does not see the dog.
False
3
inv-proof
[(((((triple1) -> rule4)) -> rule3))]
("cow" "sees" "dog" "-")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow visits the dog.
True
5
proof
[(((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("cow" "visits" "dog" "+")
((triple2 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((triple7 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The cow does not visit the dog.
False
5
inv-proof
[(((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1))]
("cow" "visits" "dog" "-")
((triple2 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((triple7 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The rabbit chases the cow.
True
7
proof
[(((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6) OR ((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6))]
("rabbit" "chases" "cow" "+")
((triple7 ((triple2 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
((triple7 ((triple7 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The rabbit does not chase the cow.
False
7
inv-proof
[(((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6) OR ((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6))]
("rabbit" "chases" "cow" "-")
((triple7 ((triple2 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
((triple7 ((triple7 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The rabbit is blue.
True
8
proof
[(((((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2) OR ((((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
("rabbit" "is" "blue" "+")
((((triple7 ((triple2 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5
((((triple7 ((triple7 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5
The rabbit is not blue.
False
8
inv-proof
[(((((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2) OR ((((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
("rabbit" "is" "blue" "-")
((((triple7 ((triple2 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5
((((triple7 ((triple7 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5
The dog is not green.
Unknown
inv-rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "green" "-")
The rabbit sees the dog.
Unknown
rconc
[@2: The rabbit sees the dog.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("rabbit" "sees" "dog" "+")
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "is" "young" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "blue" "+")
The lion is not green.
Unknown
inv-rconc
[@1: The lion is green.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("lion" "is" "green" "-")
The lion sees the dog.
Unknown
rconc
[@2: The lion sees the dog.[CWA. Example of deepest failure = (rule3 <- rule4 <- FAIL)]]
("lion" "sees" "dog" "+")
The dog is not big.
Unknown
inv-random
[@0: The dog is big.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "big" "-")
The dog visits the lion.
Unknown
random
[@0: The dog visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "lion" "+")
The lion does not chase the cow.
Unknown
inv-random
[@0: The lion chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "chases" "cow" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The cow is big.[(triple1)] The dog visits the cow.[(triple2)] The lion chases the dog.[(triple3)] The lion chases the rabbit.[(triple4)] The rabbit chases the lion.[(triple5)] The rabbit sees the cow.[(triple6)] The rabbit visits the cow.[(triple7)] @1: The cow is green.[(((triple1) -> rule4))] The cow visits the rabbit.[(((triple6) -> rule8))] @2: The cow sees the dog.[(((((triple1) -> rule4)) -> rule3))] @3: The cow visits the dog.[(((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1) OR ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1))] @4: The rabbit chases the cow.[(((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6) OR ((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6))] @5: The rabbit is blue.[(((((triple7 ((triple2 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2) OR ((((triple7 ((triple7 ((((triple1) -> rule4)) -> rule3)) -> rule1)) -> rule6)) -> rule2))]
The cow is big.
("cow" "is" "big" "+")
triple1
The dog visits the cow.
("dog" "visits" "cow" "+")
triple2
The lion chases the dog.
("lion" "chases" "dog" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple4
The rabbit chases the lion.
("rabbit" "chases" "lion" "+")
triple5
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple6
The rabbit visits the cow.
("rabbit" "visits" "cow" "+")
triple7
The cow is green.
("cow" "is" "green" "+")
((triple1) -> (rule4 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
((triple6) -> (rule8 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple1) -> (rule4 % int2))) -> (rule3 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
((triple2 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
((triple7 ((((triple1) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The cow visits the dog.
("cow" "visits" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is green.
("cow" "is" "green" "+")
int3
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
((triple7 ((triple2 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
((triple7 ((triple7 ((((triple1) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int1
The cow visits the dog.
("cow" "visits" "dog" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((triple7 ((triple2 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5
((((triple7 ((triple7 ((((triple1) -> (rule4 % int5))) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule2 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit chases the cow.
("rabbit" "chases" "cow" "+")
int2
The cow visits the dog.
("cow" "visits" "dog" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is green.
("cow" "is" "green" "+")
int5