The cat likes the rabbit. The cow is young. The cow needs the tiger. The rabbit is blue. The rabbit is rough. The rabbit likes the cat. The tiger is blue. The tiger is green. The tiger likes the cow. The tiger sees the cow. The tiger sees the rabbit. If someone is green then they need the rabbit. If the cat likes the cow and the cow sees the cat then the cat sees the cow. If someone sees the rabbit then the rabbit sees the tiger. If someone needs the rabbit and the rabbit sees the tiger then they like the tiger. If someone sees the rabbit then they like the cow. If someone likes the cow then they are green. If the cow needs the tiger then the cow sees the rabbit. If someone needs the rabbit and the rabbit sees the cat then the cat likes the tiger.
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
The cow is young.
("cow" "is" "young" "+")
The cow needs the tiger.
("cow" "needs" "tiger" "+")
The rabbit is blue.
("rabbit" "is" "blue" "+")
The rabbit is rough.
("rabbit" "is" "rough" "+")
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
The tiger is blue.
("tiger" "is" "blue" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger likes the cow.
("tiger" "likes" "cow" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If someone is green then they need the rabbit.
((("someone" "is" "green" "+")) -> ("someone" "needs" "rabbit" "+"))
If the cat likes the cow and the cow sees the cat then the cat sees the cow.
((("cat" "likes" "cow" "+") ("cow" "sees" "cat" "+")) -> ("cat" "sees" "cow" "+"))
If someone sees the rabbit then the rabbit sees the tiger.
((("someone" "sees" "rabbit" "+")) -> ("rabbit" "sees" "tiger" "+"))
If someone needs the rabbit and the rabbit sees the tiger then they like the tiger.
((("someone" "needs" "rabbit" "+") ("rabbit" "sees" "tiger" "+")) -> ("someone" "likes" "tiger" "+"))
If someone sees the rabbit then they like the cow.
((("someone" "sees" "rabbit" "+")) -> ("someone" "likes" "cow" "+"))
If someone likes the cow then they are green.
((("someone" "likes" "cow" "+")) -> ("someone" "is" "green" "+"))
If the cow needs the tiger then the cow sees the rabbit.
((("cow" "needs" "tiger" "+")) -> ("cow" "sees" "rabbit" "+"))
If someone needs the rabbit and the rabbit sees the cat then the cat likes the tiger.
((("someone" "needs" "rabbit" "+") ("rabbit" "sees" "cat" "+")) -> ("cat" "likes" "tiger" "+"))
The cat likes the rabbit.
True
1
proof
[(triple1)]
("cat" "likes" "rabbit" "+")
triple1
The rabbit is not rough.
False
1
inv-proof
[(triple5)]
("rabbit" "is" "rough" "-")
triple5
The cow sees the rabbit.
True
2
proof
[(((triple3) -> rule7))]
("cow" "sees" "rabbit" "+")
((triple3) -> (rule7 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow does not see the rabbit.
False
2
inv-proof
[(((triple3) -> rule7))]
("cow" "sees" "rabbit" "-")
((triple3) -> (rule7 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The cow likes the cow.
True
3
proof
[(((((triple3) -> rule7)) -> rule5))]
("cow" "likes" "cow" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow does not like the cow.
False
3
inv-proof
[(((((triple3) -> rule7)) -> rule5))]
("cow" "likes" "cow" "-")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The cow is green.
True
4
proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule6))]
("cow" "is" "green" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow is not green.
False
4
inv-proof
[(((((((triple3) -> rule7)) -> rule5)) -> rule6))]
("cow" "is" "green" "-")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow needs the rabbit.
True
5
proof
[(((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1))]
("cow" "needs" "rabbit" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow does not need the rabbit.
False
5
inv-proof
[(((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1))]
("cow" "needs" "rabbit" "-")
((((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow likes the tiger.
True
8
proof
[(((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4))]
("cow" "likes" "tiger" "+")
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule7 % int6))) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6
The cow does not like the tiger.
False
8
inv-proof
[(((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4))]
("cow" "likes" "tiger" "-")
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule7 % int6))) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6
The rabbit does not like the cow.
Unknown
inv-rconc
[@1: The rabbit likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("rabbit" "likes" "cow" "-")
The rabbit likes the tiger.
Unknown
rconc
[@4: The rabbit likes the tiger.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule5 <- FAIL)]]
("rabbit" "likes" "tiger" "+")
The cat does not need the rabbit.
Unknown
inv-rconc
[@3: The cat needs the rabbit.[CWA. Example of deepest failure = (rule1 <- rule6 <- rule5 <- FAIL)]]
("cat" "needs" "rabbit" "-")
The rabbit is green.
Unknown
rconc
[@2: The rabbit is green.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("rabbit" "is" "green" "+")
The cat does not like the tiger.
Unknown
inv-rconc
[@4: The cat likes the tiger.[CWA. Example of deepest failure = (rule4 <- rule1 <- rule6 <- rule5 <- FAIL)]]
("cat" "likes" "tiger" "-")
The cat sees the cow.
Unknown
rconc
[@1: The cat sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cat" "sees" "cow" "+")
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 tiger likes the rabbit.
Unknown
random
[@0: The tiger likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "rabbit" "+")
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 tiger needs the cow.
Unknown
random
[@0: The tiger needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "cow" "+")
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 sees the cat.
Unknown
random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "+")
@0: The cat likes the rabbit.[(triple1)] The cow is young.[(triple2)] The cow needs the tiger.[(triple3)] The rabbit is blue.[(triple4)] The rabbit is rough.[(triple5)] The rabbit likes the cat.[(triple6)] The tiger is blue.[(triple7)] The tiger is green.[(triple8 OR ((triple9) -> rule6) OR ((((triple11) -> rule5)) -> rule6))] The tiger likes the cow.[(triple9 OR ((triple11) -> rule5))] The tiger sees the cow.[(triple10)] The tiger sees the rabbit.[(triple11)] @1: The cow sees the rabbit.[(((triple3) -> rule7))] The rabbit sees the tiger.[(((triple11) -> rule3) OR ((((triple3) -> rule7)) -> rule3))] The tiger needs the rabbit.[(((triple8) -> rule1) OR ((((triple9) -> rule6)) -> rule1) OR ((((((triple11) -> rule5)) -> rule6)) -> rule1))] @2: The cow likes the cow.[(((((triple3) -> rule7)) -> rule5))] The tiger likes the tiger.[(((((triple8) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((triple8) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4) OR ((((((triple9) -> rule6)) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((((triple9) -> rule6)) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4) OR ((((((((triple11) -> rule5)) -> rule6)) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((((((triple11) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4))] @3: The cow is green.[(((((((triple3) -> rule7)) -> rule5)) -> rule6))] @4: The cow needs the rabbit.[(((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1))] @5: The cow likes the tiger.[(((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((triple11) -> rule3)) -> rule4) OR ((((((((((triple3) -> rule7)) -> rule5)) -> rule6)) -> rule1) ((((triple3) -> rule7)) -> rule3)) -> rule4))]
The cat likes the rabbit.
("cat" "likes" "rabbit" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow needs the tiger.
("cow" "needs" "tiger" "+")
triple3
The rabbit is blue.
("rabbit" "is" "blue" "+")
triple4
The rabbit is rough.
("rabbit" "is" "rough" "+")
triple5
The rabbit likes the cat.
("rabbit" "likes" "cat" "+")
triple6
The tiger is blue.
("tiger" "is" "blue" "+")
triple7
The tiger is green.
("tiger" "is" "green" "+")
triple8
((triple9) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
((((triple11) -> (rule5 % int2))) -> (rule6 % int1))
The tiger is green.
("tiger" "is" "green" "+")
int1
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
triple9
((triple11) -> (rule5 % int1))
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int1
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple10
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple11
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
((triple3) -> (rule7 % int1))
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
((triple11) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
((((triple3) -> (rule7 % int2))) -> (rule3 % int1))
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
((triple8) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
((((triple9) -> (rule6 % int2))) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
((((((triple11) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int1
The tiger is green.
("tiger" "is" "green" "+")
int2
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int3
The cow likes the cow.
("cow" "likes" "cow" "+")
((((triple3) -> (rule7 % int2))) -> (rule5 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int2
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
((((triple8) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
((((triple8) -> (rule1 % int4)) ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
((((((triple9) -> (rule6 % int4))) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
((((((triple9) -> (rule6 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
int5
((((((((triple11) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int3
The tiger is green.
("tiger" "is" "green" "+")
int4
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int5
((((((((triple11) -> (rule5 % int6))) -> (rule6 % int5))) -> (rule1 % int4)) ((((triple3) -> (rule7 % int3))) -> (rule3 % int2))) -> (rule4 % int1))
The tiger likes the tiger.
("tiger" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The tiger needs the rabbit.
("tiger" "needs" "rabbit" "+")
int4
The tiger is green.
("tiger" "is" "green" "+")
int5
The tiger likes the cow.
("tiger" "likes" "cow" "+")
int6
The cow is green.
("cow" "is" "green" "+")
((((((triple3) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
The cow is green.
("cow" "is" "green" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
int2
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int3
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
((((((((triple3) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int1
The cow is green.
("cow" "is" "green" "+")
int2
The cow likes the cow.
("cow" "likes" "cow" "+")
int3
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int4
The cow likes the tiger.
("cow" "likes" "tiger" "+")
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((triple11) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6
((((((((((triple3) -> (rule7 % int6))) -> (rule5 % int5))) -> (rule6 % int4))) -> (rule1 % int3)) ((((triple3) -> (rule7 % int6))) -> (rule3 % int2))) -> (rule4 % int1))
The cow likes the tiger.
("cow" "likes" "tiger" "+")
int1
The rabbit sees the tiger.
("rabbit" "sees" "tiger" "+")
int2
The cow needs the rabbit.
("cow" "needs" "rabbit" "+")
int3
The cow is green.
("cow" "is" "green" "+")
int4
The cow likes the cow.
("cow" "likes" "cow" "+")
int5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
int6