The cow is red. The cow needs the lion. The cow sees the rabbit. The dog is kind. The dog likes the lion. The dog needs the cow. The dog needs the rabbit. The dog sees the rabbit. The lion is blue. The lion is kind. The lion likes the rabbit. The lion needs the dog. The lion needs the rabbit. The rabbit is kind. The rabbit needs the lion. The rabbit sees the cow. If something likes the cow then the cow likes the lion. If something likes the rabbit and it needs the rabbit then it is green. If something is blue then it sees the rabbit. If something sees the cow then the cow likes the dog. If something sees the dog then it is blue. If something likes the dog and it needs the rabbit then the rabbit sees the dog. If something likes the lion and it likes the dog then the lion sees the dog. If something likes the dog then it needs the rabbit.
The cow is red.
("cow" "is" "red" "+")
The cow needs the lion.
("cow" "needs" "lion" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The dog is kind.
("dog" "is" "kind" "+")
The dog likes the lion.
("dog" "likes" "lion" "+")
The dog needs the cow.
("dog" "needs" "cow" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
The lion is blue.
("lion" "is" "blue" "+")
The lion is kind.
("lion" "is" "kind" "+")
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
The lion needs the dog.
("lion" "needs" "dog" "+")
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
If something likes the cow then the cow likes the lion.
((("something" "likes" "cow" "+")) -> ("cow" "likes" "lion" "+"))
If something likes the rabbit and it needs the rabbit then it is green.
((("something" "likes" "rabbit" "+") ("something" "needs" "rabbit" "+")) -> ("something" "is" "green" "+"))
If something is blue then it sees the rabbit.
((("something" "is" "blue" "+")) -> ("something" "sees" "rabbit" "+"))
If something sees the cow then the cow likes the dog.
((("something" "sees" "cow" "+")) -> ("cow" "likes" "dog" "+"))
If something sees the dog then it is blue.
((("something" "sees" "dog" "+")) -> ("something" "is" "blue" "+"))
If something likes the dog and it needs the rabbit then the rabbit sees the dog.
((("something" "likes" "dog" "+") ("something" "needs" "rabbit" "+")) -> ("rabbit" "sees" "dog" "+"))
If something likes the lion and it likes the dog then the lion sees the dog.
((("something" "likes" "lion" "+") ("something" "likes" "dog" "+")) -> ("lion" "sees" "dog" "+"))
If something likes the dog then it needs the rabbit.
((("something" "likes" "dog" "+")) -> ("something" "needs" "rabbit" "+"))
The cow is red.
True
1
proof
[(triple1)]
("cow" "is" "red" "+")
triple1
The cow does not see the rabbit.
False
1
inv-proof
[(triple3)]
("cow" "sees" "rabbit" "-")
triple3
The cow likes the dog.
True
2
proof
[(((triple16) -> rule4))]
("cow" "likes" "dog" "+")
((triple16) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The lion does not see the rabbit.
False
2
inv-proof
[(((triple9) -> rule3))]
("lion" "sees" "rabbit" "-")
((triple9) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The cow needs the rabbit.
True
3
proof
[(((((triple16) -> rule4)) -> rule8))]
("cow" "needs" "rabbit" "+")
((((triple16) -> (rule4 % int2))) -> (rule8 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The cow does not need the rabbit.
False
3
inv-proof
[(((((triple16) -> rule4)) -> rule8))]
("cow" "needs" "rabbit" "-")
((((triple16) -> (rule4 % int2))) -> (rule8 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The rabbit sees the dog.
True
6
proof
[(((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6))]
("rabbit" "sees" "dog" "+")
((((triple16) -> (rule4 % int3)) ((((triple16) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The rabbit does not see the dog.
False
6
inv-proof
[(((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6))]
("rabbit" "sees" "dog" "-")
((((triple16) -> (rule4 % int3)) ((((triple16) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The rabbit is blue.
True
7
proof
[(((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5))]
("rabbit" "is" "blue" "+")
((((((triple16) -> (rule4 % int4)) ((((triple16) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The rabbit is not blue.
False
7
inv-proof
[(((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5))]
("rabbit" "is" "blue" "-")
((((((triple16) -> (rule4 % int4)) ((((triple16) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The rabbit sees the rabbit.
True
8
proof
[(((((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5)) -> rule3))]
("rabbit" "sees" "rabbit" "+")
((((((((triple16) -> (rule4 % int5)) ((((triple16) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The rabbit does not see the rabbit.
False
8
inv-proof
[(((((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5)) -> rule3))]
("rabbit" "sees" "rabbit" "-")
((((((((triple16) -> (rule4 % int5)) ((((triple16) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5
The cow does not like the lion.
Unknown
inv-rconc
[@1: The cow likes the lion.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "likes" "lion" "-")
The dog is green.
Unknown
rconc
[@1: The dog is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "green" "+")
The lion does not see the dog.
Unknown
inv-rconc
[@2: The lion sees the dog.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("lion" "sees" "dog" "-")
The rabbit is green.
Unknown
rconc
[@1: The rabbit is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "green" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "blue" "-")
The cow is blue.
Unknown
rconc
[@1: The cow is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "blue" "+")
The cow is not cold.
Unknown
inv-random
[@0: The cow is cold.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "cold" "-")
The lion needs the cow.
Unknown
random
[@0: The lion needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "needs" "cow" "+")
The rabbit does not like the cow.
Unknown
inv-random
[@0: The rabbit likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "cow" "-")
The cow needs the cow.
Unknown
random
[@0: The cow needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "cow" "+")
The rabbit is not cold.
Unknown
inv-random
[@0: The rabbit is cold.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "cold" "-")
The rabbit needs the cow.
Unknown
random
[@0: The rabbit needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "cow" "+")
@0: The cow is red.[(triple1)] The cow needs the lion.[(triple2)] The cow sees the rabbit.[(triple3)] The dog is kind.[(triple4)] The dog likes the lion.[(triple5)] The dog needs the cow.[(triple6)] The dog needs the rabbit.[(triple7)] The dog sees the rabbit.[(triple8)] The lion is blue.[(triple9)] The lion is kind.[(triple10)] The lion likes the rabbit.[(triple11)] The lion needs the dog.[(triple12)] The lion needs the rabbit.[(triple13)] The rabbit is kind.[(triple14)] The rabbit needs the lion.[(triple15)] The rabbit sees the cow.[(triple16)] @1: The cow likes the dog.[(((triple16) -> rule4))] The lion is green.[(((triple11 triple13) -> rule2))] The lion sees the rabbit.[(((triple9) -> rule3))] @2: The cow needs the rabbit.[(((((triple16) -> rule4)) -> rule8))] @3: The rabbit sees the dog.[(((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6))] @4: The rabbit is blue.[(((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5))] @5: The rabbit sees the rabbit.[(((((((((triple16) -> rule4) ((((triple16) -> rule4)) -> rule8)) -> rule6)) -> rule5)) -> rule3))]
The cow is red.
("cow" "is" "red" "+")
triple1
The cow needs the lion.
("cow" "needs" "lion" "+")
triple2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple3
The dog is kind.
("dog" "is" "kind" "+")
triple4
The dog likes the lion.
("dog" "likes" "lion" "+")
triple5
The dog needs the cow.
("dog" "needs" "cow" "+")
triple6
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple7
The dog sees the rabbit.
("dog" "sees" "rabbit" "+")
triple8
The lion is blue.
("lion" "is" "blue" "+")
triple9
The lion is kind.
("lion" "is" "kind" "+")
triple10
The lion likes the rabbit.
("lion" "likes" "rabbit" "+")
triple11
The lion needs the dog.
("lion" "needs" "dog" "+")
triple12
The lion needs the rabbit.
("lion" "needs" "rabbit" "+")
triple13
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple14
The rabbit needs the lion.
("rabbit" "needs" "lion" "+")
triple15
The rabbit sees the cow.
("rabbit" "sees" "cow" "+")
triple16
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple16) -> (rule4 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The lion is green.
("lion" "is" "green" "+")
((triple11 triple13) -> (rule2 % int1))
The lion is green.
("lion" "is" "green" "+")
int1
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
((triple9) -> (rule3 % int1))
The lion sees the rabbit.
("lion" "sees" "rabbit" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((((triple16) -> (rule4 % int2))) -> (rule8 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
((((triple16) -> (rule4 % int3)) ((((triple16) -> (rule4 % int3))) -> (rule8 % int2))) -> (rule6 % int1))
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int1
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int2
The cow likes the dog.
("cow" "likes" "dog" "+")
int3
The rabbit is blue.
("rabbit" "is" "blue" "+")
((((((triple16) -> (rule4 % int4)) ((((triple16) -> (rule4 % int4))) -> (rule8 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
The rabbit is blue.
("rabbit" "is" "blue" "+")
int1
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow likes the dog.
("cow" "likes" "dog" "+")
int4
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
((((((((triple16) -> (rule4 % int5)) ((((triple16) -> (rule4 % int5))) -> (rule8 % int4))) -> (rule6 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit sees the rabbit.
("rabbit" "sees" "rabbit" "+")
int1
The rabbit is blue.
("rabbit" "is" "blue" "+")
int2
The rabbit sees the dog.
("rabbit" "sees" "dog" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int4
The cow likes the dog.
("cow" "likes" "dog" "+")
int5