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