The dog chases the mouse. The dog chases the rabbit. The dog needs the rabbit. The dog sees the tiger. The mouse chases the dog. The mouse chases the tiger. The mouse needs the dog. The rabbit chases the mouse. The rabbit chases the tiger. The rabbit is round. The tiger is cold. The tiger needs the dog. If something needs the dog then it chases the tiger. If something chases the tiger then it needs the tiger. If something is nice then it is rough. If something is kind and it needs the mouse then it sees the rabbit. If something chases the dog and it chases the rabbit then the dog chases the tiger. If something sees the mouse then the mouse sees the tiger. If something is nice and it needs the tiger then the tiger chases the mouse. If something sees the mouse and the mouse needs the dog then the dog chases the tiger.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something needs the dog then it chases the tiger.
((("something" "needs" "dog" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the tiger then it needs the tiger.
((("something" "chases" "tiger" "+")) -> ("something" "needs" "tiger" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is kind and it needs the mouse then it sees the rabbit.
((("something" "is" "kind" "+") ("something" "needs" "mouse" "+")) -> ("something" "sees" "rabbit" "+"))
If something chases the dog and it chases the rabbit then the dog chases the tiger.
((("something" "chases" "dog" "+") ("something" "chases" "rabbit" "+")) -> ("dog" "chases" "tiger" "+"))
If something sees the mouse then the mouse sees the tiger.
((("something" "sees" "mouse" "+")) -> ("mouse" "sees" "tiger" "+"))
If something is nice and it needs the tiger then the tiger chases the mouse.
((("something" "is" "nice" "+") ("something" "needs" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If something sees the mouse and the mouse needs the dog then the dog chases the tiger.
((("something" "sees" "mouse" "+") ("mouse" "needs" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
The mouse needs the dog.
True
1
proof
[(triple7)]
("mouse" "needs" "dog" "+")
triple7
The rabbit does not chase the mouse.
False
1
inv-proof
[(triple8)]
("rabbit" "chases" "mouse" "-")
triple8
The tiger chases the tiger.
True
2
proof
[(((triple12) -> rule1))]
("tiger" "chases" "tiger" "+")
((triple12) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The rabbit does not need the tiger.
False
2
inv-proof
[(((triple9) -> rule2))]
("rabbit" "needs" "tiger" "-")
((triple9) -> (rule2 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger needs the tiger.
True
3
proof
[(((((triple12) -> rule1)) -> rule2))]
("tiger" "needs" "tiger" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger does not need the tiger.
False
3
inv-proof
[(((((triple12) -> rule1)) -> rule2))]
("tiger" "needs" "tiger" "-")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The rabbit is not rough.
Unknown
inv-rconc
[@1: The rabbit is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("rabbit" "is" "rough" "-")
The rabbit sees the rabbit.
Unknown
rconc
[@1: The rabbit sees the rabbit.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "sees" "rabbit" "+")
The dog is not rough.
Unknown
inv-rconc
[@1: The dog is rough.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "rough" "-")
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 need the mouse.
Unknown
inv-random
[@0: The dog needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "mouse" "-")
The tiger sees the dog.
Unknown
random
[@0: The tiger sees the dog.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "dog" "+")
@0: The dog chases the mouse.[(triple1)] The dog chases the rabbit.[(triple2)] The dog needs the rabbit.[(triple3)] The dog sees the tiger.[(triple4)] The mouse chases the dog.[(triple5)] The mouse chases the tiger.[(triple6 OR ((triple7) -> rule1))] The mouse needs the dog.[(triple7)] The rabbit chases the mouse.[(triple8)] The rabbit chases the tiger.[(triple9)] The rabbit is round.[(triple10)] The tiger is cold.[(triple11)] The tiger needs the dog.[(triple12)] @1: The mouse needs the tiger.[(((triple6) -> rule2) OR ((((triple7) -> rule1)) -> rule2))] The rabbit needs the tiger.[(((triple9) -> rule2))] The tiger chases the tiger.[(((triple12) -> rule1))] @2: The tiger needs the tiger.[(((((triple12) -> rule1)) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
triple2
The dog needs the rabbit.
("dog" "needs" "rabbit" "+")
triple3
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple4
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple5
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple6
((triple7) -> (rule1 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple7
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple8
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple9
The rabbit is round.
("rabbit" "is" "round" "+")
triple10
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple12
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
((triple6) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
((((triple7) -> (rule1 % int2))) -> (rule2 % int1))
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
int1
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int2
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
((triple9) -> (rule2 % int1))
The rabbit needs the tiger.
("rabbit" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple12) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
((((triple12) -> (rule1 % int2))) -> (rule2 % int1))
The tiger needs the tiger.
("tiger" "needs" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2