The dog does not eat the mouse. The dog is round. The dog visits the rabbit. The mouse visits the tiger. The rabbit chases the mouse. The rabbit does not eat the dog. The rabbit is young. The rabbit visits the tiger. The tiger is not kind. The tiger visits the dog. The tiger does not visit the mouse. If someone eats the tiger then they do not chase the tiger. If someone is blue then they eat the mouse. If someone visits the dog then they are blue. If someone visits the dog and they are not round then they are young. If someone is blue and they eat the mouse then the mouse visits the dog.
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
The dog is round.
("dog" "is" "round" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
The rabbit is young.
("rabbit" "is" "young" "+")
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
The tiger is not kind.
("tiger" "is" "kind" "-")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
If someone eats the tiger then they do not chase the tiger.
((("someone" "eats" "tiger" "+")) -> ("someone" "chases" "tiger" "-"))
If someone is blue then they eat the mouse.
((("someone" "is" "blue" "+")) -> ("someone" "eats" "mouse" "+"))
If someone visits the dog then they are blue.
((("someone" "visits" "dog" "+")) -> ("someone" "is" "blue" "+"))
If someone visits the dog and they are not round then they are young.
((("someone" "visits" "dog" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "young" "+"))
If someone is blue and they eat the mouse then the mouse visits the dog.
((("someone" "is" "blue" "+") ("someone" "eats" "mouse" "+")) -> ("mouse" "visits" "dog" "+"))
The tiger visits the dog.
True
1
proof
[(triple10)]
("tiger" "visits" "dog" "+")
triple10
The dog is not round.
False
1
inv-proof
[(triple2)]
("dog" "is" "round" "-")
triple2
The tiger is blue.
True
2
proof
[(((triple10) -> rule3))]
("tiger" "is" "blue" "+")
((triple10) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger is not blue.
False
2
inv-proof
[(((triple10) -> rule3))]
("tiger" "is" "blue" "-")
((triple10) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger eats the mouse.
True
3
proof
[(((((triple10) -> rule3)) -> rule2))]
("tiger" "eats" "mouse" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The tiger does not eat the mouse.
False
3
inv-proof
[(((((triple10) -> rule3)) -> rule2))]
("tiger" "eats" "mouse" "-")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The mouse visits the dog.
True
6
proof
[(((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5))]
("mouse" "visits" "dog" "+")
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The mouse does not visit the dog.
False
6
inv-proof
[(((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5))]
("mouse" "visits" "dog" "-")
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The mouse is blue.
True
7
proof
[(((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "blue" "+")
((((((triple10) -> (rule3 % int4)) ((((triple10) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
int4
The mouse is not blue.
False
7
inv-proof
[(((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3))]
("mouse" "is" "blue" "-")
((((((triple10) -> (rule3 % int4)) ((((triple10) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
int4
The mouse eats the mouse.
True
8
proof
[(((((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "eats" "mouse" "+")
((((((((triple10) -> (rule3 % int5)) ((((triple10) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int4
The tiger is blue.
("tiger" "is" "blue" "+")
int5
The mouse does not eat the mouse.
False
8
inv-proof
[(((((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3)) -> rule2))]
("mouse" "eats" "mouse" "-")
((((((((triple10) -> (rule3 % int5)) ((((triple10) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int4
The tiger is blue.
("tiger" "is" "blue" "+")
int5
The rabbit is not blue.
Unknown
inv-rconc
[@1: The rabbit is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "blue" "-")
The rabbit eats the mouse.
Unknown
rconc
[@2: The rabbit eats the mouse.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("rabbit" "eats" "mouse" "+")
The dog is not blue.
Unknown
inv-rconc
[@1: The dog is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "blue" "-")
The mouse is young.
Unknown
rconc
[@1: The mouse is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "young" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("tiger" "is" "young" "-")
The dog is young.
Unknown
rconc
[@1: The dog is young.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "young" "+")
The mouse does not chase the mouse.
Unknown
inv-random
[@0: The mouse chases the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "mouse" "-")
The tiger visits the rabbit.
Unknown
random
[@0: The tiger visits the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "rabbit" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The tiger chases the dog.
Unknown
random
[@0: The tiger chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "dog" "+")
The dog does not eat the rabbit.
Unknown
inv-random
[@0: The dog eats the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "rabbit" "-")
The dog visits the dog.
Unknown
random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "+")
@0: The dog does not eat the mouse.[(triple1)] The dog is round.[(triple2)] The dog visits the rabbit.[(triple3)] The mouse visits the tiger.[(triple4)] The rabbit chases the mouse.[(triple5)] The rabbit does not eat the dog.[(triple6)] The rabbit is young.[(triple7)] The rabbit visits the tiger.[(triple8)] The tiger does not visit the mouse.[(triple11)] The tiger is not kind.[(triple9)] The tiger visits the dog.[(triple10)] @1: The tiger is blue.[(((triple10) -> rule3))] @2: The tiger eats the mouse.[(((((triple10) -> rule3)) -> rule2))] @3: The mouse visits the dog.[(((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5))] @4: The mouse is blue.[(((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3))] @5: The mouse eats the mouse.[(((((((((triple10) -> rule3) ((((triple10) -> rule3)) -> rule2)) -> rule5)) -> rule3)) -> rule2))]
The dog does not eat the mouse.
("dog" "eats" "mouse" "-")
triple1
The dog is round.
("dog" "is" "round" "+")
triple2
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple3
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple4
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple5
The rabbit does not eat the dog.
("rabbit" "eats" "dog" "-")
triple6
The rabbit is young.
("rabbit" "is" "young" "+")
triple7
The rabbit visits the tiger.
("rabbit" "visits" "tiger" "+")
triple8
The tiger does not visit the mouse.
("tiger" "visits" "mouse" "-")
triple11
The tiger is not kind.
("tiger" "is" "kind" "-")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The tiger is blue.
("tiger" "is" "blue" "+")
((triple10) -> (rule3 % int1))
The tiger is blue.
("tiger" "is" "blue" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
((((triple10) -> (rule3 % int2))) -> (rule2 % int1))
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int1
The tiger is blue.
("tiger" "is" "blue" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
((((triple10) -> (rule3 % int3)) ((((triple10) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int1
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int2
The tiger is blue.
("tiger" "is" "blue" "+")
int3
The mouse is blue.
("mouse" "is" "blue" "+")
((((((triple10) -> (rule3 % int4)) ((((triple10) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule3 % int1))
The mouse is blue.
("mouse" "is" "blue" "+")
int1
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int2
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int3
The tiger is blue.
("tiger" "is" "blue" "+")
int4
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
((((((((triple10) -> (rule3 % int5)) ((((triple10) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
The mouse eats the mouse.
("mouse" "eats" "mouse" "+")
int1
The mouse is blue.
("mouse" "is" "blue" "+")
int2
The mouse visits the dog.
("mouse" "visits" "dog" "+")
int3
The tiger eats the mouse.
("tiger" "eats" "mouse" "+")
int4
The tiger is blue.
("tiger" "is" "blue" "+")
int5