The cat is green. The cow is young. The cow likes the lion. The cow needs the cat. The dog sees the lion. The lion needs the cow. The lion sees the cat. If someone likes the lion then they like the dog. If someone is young then they like the cow. If the cow is young and the cow sees the dog then the dog is young. If someone likes the cow then they see the dog. If someone sees the cat then the cat is blue.
The cat is green.
("cat" "is" "green" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the lion.
("cow" "likes" "lion" "+")
The cow needs the cat.
("cow" "needs" "cat" "+")
The dog sees the lion.
("dog" "sees" "lion" "+")
The lion needs the cow.
("lion" "needs" "cow" "+")
The lion sees the cat.
("lion" "sees" "cat" "+")
If someone likes the lion then they like the dog.
((("someone" "likes" "lion" "+")) -> ("someone" "likes" "dog" "+"))
If someone is young then they like the cow.
((("someone" "is" "young" "+")) -> ("someone" "likes" "cow" "+"))
If the cow is young and the cow sees the dog then the dog is young.
((("cow" "is" "young" "+") ("cow" "sees" "dog" "+")) -> ("dog" "is" "young" "+"))
If someone likes the cow then they see the dog.
((("someone" "likes" "cow" "+")) -> ("someone" "sees" "dog" "+"))
If someone sees the cat then the cat is blue.
((("someone" "sees" "cat" "+")) -> ("cat" "is" "blue" "+"))
The cow likes the lion.
True
1
proof
[(triple3)]
("cow" "likes" "lion" "+")
triple3
The cat is not green.
False
1
inv-proof
[(triple1)]
("cat" "is" "green" "-")
triple1
The cow likes the dog.
True
2
proof
[(((triple3) -> rule1))]
("cow" "likes" "dog" "+")
((triple3) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow does not like the cow.
False
2
inv-proof
[(((triple2) -> rule2))]
("cow" "likes" "cow" "-")
((triple2) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the dog.
True
3
proof
[(((((triple2) -> rule2)) -> rule4))]
("cow" "sees" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow does not see the dog.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule4))]
("cow" "sees" "dog" "-")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The dog is young.
True
5
proof
[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3))]
("dog" "is" "young" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The dog is not young.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3))]
("dog" "is" "young" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The dog likes the cow.
True
6
proof
[(((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2))]
("dog" "likes" "cow" "+")
((((triple2 ((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The dog does not like the cow.
False
6
inv-proof
[(((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2))]
("dog" "likes" "cow" "-")
((((triple2 ((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The dog sees the dog.
True
7
proof
[(((((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2)) -> rule4))]
("dog" "sees" "dog" "+")
((((((triple2 ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The dog does not see the dog.
False
7
inv-proof
[(((((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2)) -> rule4))]
("dog" "sees" "dog" "-")
((((((triple2 ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The dog does not like the dog.
Unknown
inv-rconc
[@1: The dog likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "likes" "dog" "-")
The cat sees the dog.
Unknown
rconc
[@2: The cat sees the dog.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("cat" "sees" "dog" "+")
The lion does not see the dog.
Unknown
inv-rconc
[@2: The lion sees the dog.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("lion" "sees" "dog" "-")
The lion likes the cow.
Unknown
rconc
[@1: The lion likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("lion" "likes" "cow" "+")
The cat does not like the dog.
Unknown
inv-rconc
[@1: The cat likes the dog.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "likes" "dog" "-")
The cat likes the cow.
Unknown
rconc
[@1: The cat likes the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "likes" "cow" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The dog likes the lion.
Unknown
random
[@0: The dog likes the lion.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "lion" "+")
The dog does not need the cow.
Unknown
inv-random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
The lion is not nice.
Unknown
inv-random
[@0: The lion is nice.[CWA. Example of deepest failure = (FAIL)]]
("lion" "is" "nice" "-")
The dog sees the cow.
Unknown
random
[@0: The dog sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "sees" "cow" "+")
@0: The cat is green.[(triple1)] The cow is young.[(triple2)] The cow likes the lion.[(triple3)] The cow needs the cat.[(triple4)] The dog sees the lion.[(triple5)] The lion needs the cow.[(triple6)] The lion sees the cat.[(triple7)] @1: The cat is blue.[(((triple7) -> rule5))] The cow likes the cow.[(((triple2) -> rule2))] The cow likes the dog.[(((triple3) -> rule1))] @2: The cow sees the dog.[(((((triple2) -> rule2)) -> rule4))] @3: The dog is young.[(((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3))] @4: The dog likes the cow.[(((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2))] @5: The dog sees the dog.[(((((((triple2 ((((triple2) -> rule2)) -> rule4)) -> rule3)) -> rule2)) -> rule4))]
The cat is green.
("cat" "is" "green" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow likes the lion.
("cow" "likes" "lion" "+")
triple3
The cow needs the cat.
("cow" "needs" "cat" "+")
triple4
The dog sees the lion.
("dog" "sees" "lion" "+")
triple5
The lion needs the cow.
("lion" "needs" "cow" "+")
triple6
The lion sees the cat.
("lion" "sees" "cat" "+")
triple7
The cat is blue.
("cat" "is" "blue" "+")
((triple7) -> (rule5 % int1))
The cat is blue.
("cat" "is" "blue" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple2) -> (rule2 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow likes the dog.
("cow" "likes" "dog" "+")
((triple3) -> (rule1 % int1))
The cow likes the dog.
("cow" "likes" "dog" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The dog is young.
("dog" "is" "young" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The dog likes the cow.
("dog" "likes" "cow" "+")
((((triple2 ((((triple2) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The dog likes the cow.
("dog" "likes" "cow" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((triple2 ((((triple2) -> (rule2 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog likes the cow.
("dog" "likes" "cow" "+")
int2
The dog is young.
("dog" "is" "young" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5