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