The cat is round. The cow is young. The cow sees the rabbit. The lion chases the rabbit. The lion is blue. The lion is round. The lion likes the rabbit. The lion sees the cat. The lion sees the rabbit. The rabbit sees the lion. If someone chases the cat then they see the cow. If someone chases the cat and they see the cow then the cat likes the cow. If someone is blue and they like the cow then they like the lion. If someone likes the cow and they do not chase the lion then the cow likes the lion. If someone likes the cow then they like the cat. If someone sees the rabbit then they like the cat. Cold people are round. If someone likes the cat then they chase the cat. If someone chases the lion and the lion does not chase the cow then they like the cow.
The cat is round.
("cat" "is" "round" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is round.
("lion" "is" "round" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
If someone chases the cat then they see the cow.
((("someone" "chases" "cat" "+")) -> ("someone" "sees" "cow" "+"))
If someone chases the cat and they see the cow then the cat likes the cow.
((("someone" "chases" "cat" "+") ("someone" "sees" "cow" "+")) -> ("cat" "likes" "cow" "+"))
If someone is blue and they like the cow then they like the lion.
((("someone" "is" "blue" "+") ("someone" "likes" "cow" "+")) -> ("someone" "likes" "lion" "+"))
If someone likes the cow and they do not chase the lion then the cow likes the lion.
((("someone" "likes" "cow" "+") ("someone" "chases" "lion" "~")) -> ("cow" "likes" "lion" "+"))
If someone likes the cow then they like the cat.
((("someone" "likes" "cow" "+")) -> ("someone" "likes" "cat" "+"))
If someone sees the rabbit then they like the cat.
((("someone" "sees" "rabbit" "+")) -> ("someone" "likes" "cat" "+"))
Cold people are round.
((("someone" "is" "cold" "+")) -> ("someone" "is" "round" "+"))
If someone likes the cat then they chase the cat.
((("someone" "likes" "cat" "+")) -> ("someone" "chases" "cat" "+"))
If someone chases the lion and the lion does not chase the cow then they like the cow.
((("someone" "chases" "lion" "+") ("lion" "chases" "cow" "~")) -> ("someone" "likes" "cow" "+"))
The cow is young.
True
1
proof
[(triple2)]
("cow" "is" "young" "+")
triple2
The cow is not young.
False
1
inv-proof
[(triple2)]
("cow" "is" "young" "-")
triple2
The cow likes the cat.
True
2
proof
[(((triple3) -> rule6))]
("cow" "likes" "cat" "+")
((triple3) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The cow does not like the cat.
False
2
inv-proof
[(((triple3) -> rule6))]
("cow" "likes" "cat" "-")
((triple3) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The lion chases the cat.
True
3
proof
[(((((triple9) -> rule6)) -> rule8))]
("lion" "chases" "cat" "+")
((((triple9) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The lion does not chase the cat.
False
3
inv-proof
[(((((triple9) -> rule6)) -> rule8))]
("lion" "chases" "cat" "-")
((((triple9) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The cow sees the cow.
True
4
proof
[(((((((triple3) -> rule6)) -> rule8)) -> rule1))]
("cow" "sees" "cow" "+")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
int3
The lion does not see the cow.
False
4
inv-proof
[(((((((triple9) -> rule6)) -> rule8)) -> rule1))]
("lion" "sees" "cow" "-")
((((((triple9) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
int3
The cat likes the cow.
True
8
proof
[(((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2) OR ((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2))]
("cat" "likes" "cow" "+")
((((((triple3) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple3) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cow likes the cat.
("cow" "likes" "cat" "+")
int4
((((((triple9) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The lion likes the cat.
("lion" "likes" "cat" "+")
int4
The cat does not like the cow.
False
8
inv-proof
[(((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2) OR ((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2))]
("cat" "likes" "cow" "-")
((((((triple3) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple3) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cow likes the cat.
("cow" "likes" "cat" "+")
int4
((((((triple9) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The lion likes the cat.
("lion" "likes" "cat" "+")
int4
The cat likes the cat.
True
9
proof
[(((((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5) OR ((((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5))]
("cat" "likes" "cat" "+")
((((((((triple3) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple3) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The cow likes the cat.
("cow" "likes" "cat" "+")
int5
((((((((triple9) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple9) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion chases the cat.
("lion" "chases" "cat" "+")
int4
The lion likes the cat.
("lion" "likes" "cat" "+")
int5
The cat does not like the cat.
False
9
inv-proof
[(((((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5) OR ((((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5))]
("cat" "likes" "cat" "-")
((((((((triple3) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple3) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The cow likes the cat.
("cow" "likes" "cat" "+")
int5
((((((((triple9) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple9) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion chases the cat.
("lion" "chases" "cat" "+")
int4
The lion likes the cat.
("lion" "likes" "cat" "+")
int5
The rabbit does not like the cow.
Unknown
inv-rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("rabbit" "likes" "cow" "-")
The cat likes the lion.
Unknown
rconc
[@1: The cat likes the lion.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("cat" "likes" "lion" "+")
The lion does not like the cow.
Unknown
inv-rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("lion" "likes" "cow" "-")
The rabbit chases the cat.
Unknown
rconc
[@3: The rabbit chases the cat.[CWA. Example of deepest failure = (rule8 <- rule5 <- rule9 <- FAIL)]]
("rabbit" "chases" "cat" "+")
The cow does not like the cow.
Unknown
inv-rconc
[@1: The cow likes the cow.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("cow" "likes" "cow" "-")
The rabbit is round.
Unknown
rconc
[@1: The rabbit is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("rabbit" "is" "round" "+")
The cat does not see the rabbit.
Unknown
inv-random
[@0: The cat sees the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "rabbit" "-")
The cat is young.
Unknown
random
[@0: The cat is young.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "young" "+")
The cow does not like the rabbit.
Unknown
inv-random
[@0: The cow likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "rabbit" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow does not see the cat.
Unknown
inv-random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
@0: The cat is round.[(triple1)] The cow is young.[(triple2)] The cow sees the rabbit.[(triple3)] The lion chases the rabbit.[(triple4)] The lion is blue.[(triple5)] The lion is round.[(triple6)] The lion likes the rabbit.[(triple7)] The lion sees the cat.[(triple8)] The lion sees the rabbit.[(triple9)] The rabbit sees the lion.[(triple10)] @1: The cow likes the cat.[(((triple3) -> rule6))] The lion likes the cat.[(((triple9) -> rule6))] @2: The cow chases the cat.[(((((triple3) -> rule6)) -> rule8))] The lion chases the cat.[(((((triple9) -> rule6)) -> rule8))] @3: The cow sees the cow.[(((((((triple3) -> rule6)) -> rule8)) -> rule1))] The lion sees the cow.[(((((((triple9) -> rule6)) -> rule8)) -> rule1))] @4: The cat likes the cow.[(((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2) OR ((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2))] @5: The cat likes the cat.[(((((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5) OR ((((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5))] @6: The cat chases the cat.[(((((((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5)) -> rule8) OR ((((((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5)) -> rule8))] @7: The cat sees the cow.[(((((((((((((triple3) -> rule6)) -> rule8) ((((((triple3) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5)) -> rule8)) -> rule1) OR ((((((((((((triple9) -> rule6)) -> rule8) ((((((triple9) -> rule6)) -> rule8)) -> rule1)) -> rule2)) -> rule5)) -> rule8)) -> rule1))]
The cat is round.
("cat" "is" "round" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple3
The lion chases the rabbit.
("lion" "chases" "rabbit" "+")
triple4
The lion is blue.
("lion" "is" "blue" "+")
triple5
The lion is round.
("lion" "is" "round" "+")
triple6
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple7
The lion sees the cat.
("lion" "sees" "cat" "+")
triple8
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
triple9
The rabbit sees the lion.
("rabbit" "sees" "lion" "+")
triple10
The cow likes the cat.
("cow" "likes" "cat" "+")
((triple3) -> (rule6 % int1))
The cow likes the cat.
("cow" "likes" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
((triple9) -> (rule6 % int1))
The lion likes the cat.
("lion" "likes" "cat" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
((((triple3) -> (rule6 % int2))) -> (rule8 % int1))
The cow chases the cat.
("cow" "chases" "cat" "+")
int1
The cow likes the cat.
("cow" "likes" "cat" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
((((triple9) -> (rule6 % int2))) -> (rule8 % int1))
The lion chases the cat.
("lion" "chases" "cat" "+")
int1
The lion likes the cat.
("lion" "likes" "cat" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((triple3) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the cat.
("cow" "chases" "cat" "+")
int2
The cow likes the cat.
("cow" "likes" "cat" "+")
int3
The lion sees the cow.
("lion" "sees" "cow" "+")
((((((triple9) -> (rule6 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The lion sees the cow.
("lion" "sees" "cow" "+")
int1
The lion chases the cat.
("lion" "chases" "cat" "+")
int2
The lion likes the cat.
("lion" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
((((((triple3) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple3) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow chases the cat.
("cow" "chases" "cat" "+")
int3
The cow likes the cat.
("cow" "likes" "cat" "+")
int4
((((((triple9) -> (rule6 % int4))) -> (rule8 % int3)) ((((((triple9) -> (rule6 % int4))) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
The cat likes the cow.
("cat" "likes" "cow" "+")
int1
The lion sees the cow.
("lion" "sees" "cow" "+")
int2
The lion chases the cat.
("lion" "chases" "cat" "+")
int3
The lion likes the cat.
("lion" "likes" "cat" "+")
int4
The cat likes the cat.
("cat" "likes" "cat" "+")
((((((((triple3) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple3) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3
The cow chases the cat.
("cow" "chases" "cat" "+")
int4
The cow likes the cat.
("cow" "likes" "cat" "+")
int5
((((((((triple9) -> (rule6 % int5))) -> (rule8 % int4)) ((((((triple9) -> (rule6 % int5))) -> (rule8 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The cat likes the cat.
("cat" "likes" "cat" "+")
int1
The cat likes the cow.
("cat" "likes" "cow" "+")
int2
The lion sees the cow.
("lion" "sees" "cow" "+")
int3
The lion chases the cat.
("lion" "chases" "cat" "+")
int4
The lion likes the cat.
("lion" "likes" "cat" "+")
int5
The cat chases the cat.
("cat" "chases" "cat" "+")
((((((((((triple3) -> (rule6 % int6))) -> (rule8 % int5)) ((((((triple3) -> (rule6 % int6))) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The cow sees the cow.
("cow" "sees" "cow" "+")
int4
The cow chases the cat.
("cow" "chases" "cat" "+")
int5
The cow likes the cat.
("cow" "likes" "cat" "+")
int6
((((((((((triple9) -> (rule6 % int6))) -> (rule8 % int5)) ((((((triple9) -> (rule6 % int6))) -> (rule8 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
The cat chases the cat.
("cat" "chases" "cat" "+")
int1
The cat likes the cat.
("cat" "likes" "cat" "+")
int2
The cat likes the cow.
("cat" "likes" "cow" "+")
int3
The lion sees the cow.
("lion" "sees" "cow" "+")
int4
The lion chases the cat.
("lion" "chases" "cat" "+")
int5
The lion likes the cat.
("lion" "likes" "cat" "+")
int6
The cat sees the cow.
("cat" "sees" "cow" "+")
((((((((((((triple3) -> (rule6 % int7))) -> (rule8 % int6)) ((((((triple3) -> (rule6 % int7))) -> (rule8 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
int4
The cow sees the cow.
("cow" "sees" "cow" "+")
int5
The cow chases the cat.
("cow" "chases" "cat" "+")
int6
The cow likes the cat.
("cow" "likes" "cat" "+")
int7
((((((((((((triple9) -> (rule6 % int7))) -> (rule8 % int6)) ((((((triple9) -> (rule6 % int7))) -> (rule8 % int6))) -> (rule1 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule1 % int1))
The cat sees the cow.
("cat" "sees" "cow" "+")
int1
The cat chases the cat.
("cat" "chases" "cat" "+")
int2
The cat likes the cat.
("cat" "likes" "cat" "+")
int3
The cat likes the cow.
("cat" "likes" "cow" "+")
int4
The lion sees the cow.
("lion" "sees" "cow" "+")
int5
The lion chases the cat.
("lion" "chases" "cat" "+")
int6
The lion likes the cat.
("lion" "likes" "cat" "+")
int7