The dog chases the mouse. The dog is blue. The dog needs the mouse. The mouse needs the dog. The mouse needs the rabbit. The mouse needs the tiger. The rabbit is not kind. The rabbit likes the mouse. The rabbit needs the dog. The tiger does not chase the dog. The tiger is cold. The tiger is kind. The tiger is red. The tiger is rough. The tiger needs the mouse. The tiger does not need the rabbit. If the mouse is rough and the mouse likes the rabbit then the rabbit is not red. If the rabbit chases the mouse then the mouse is blue. If something needs the dog and it needs the rabbit then the dog chases the rabbit. If the dog likes the rabbit and the rabbit needs the mouse then the dog is red. If something likes the dog then the dog chases the tiger. If something likes the dog and it needs the tiger then the dog does not need the tiger. If something chases the tiger then the tiger chases the rabbit. If something chases the rabbit and the rabbit likes the mouse then it likes the dog. If something needs the dog and it is not red then it does not like the dog.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is blue.
("dog" "is" "blue" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The rabbit is not kind.
("rabbit" "is" "kind" "-")
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
The tiger is cold.
("tiger" "is" "cold" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is red.
("tiger" "is" "red" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
If the mouse is rough and the mouse likes the rabbit then the rabbit is not red.
((("mouse" "is" "rough" "+") ("mouse" "likes" "rabbit" "+")) -> ("rabbit" "is" "red" "-"))
If the rabbit chases the mouse then the mouse is blue.
((("rabbit" "chases" "mouse" "+")) -> ("mouse" "is" "blue" "+"))
If something needs the dog and it needs the rabbit then the dog chases the rabbit.
((("something" "needs" "dog" "+") ("something" "needs" "rabbit" "+")) -> ("dog" "chases" "rabbit" "+"))
If the dog likes the rabbit and the rabbit needs the mouse then the dog is red.
((("dog" "likes" "rabbit" "+") ("rabbit" "needs" "mouse" "+")) -> ("dog" "is" "red" "+"))
If something likes the dog then the dog chases the tiger.
((("something" "likes" "dog" "+")) -> ("dog" "chases" "tiger" "+"))
If something likes the dog and it needs the tiger then the dog does not need the tiger.
((("something" "likes" "dog" "+") ("something" "needs" "tiger" "+")) -> ("dog" "needs" "tiger" "-"))
If something chases the tiger then the tiger chases the rabbit.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something chases the rabbit and the rabbit likes the mouse then it likes the dog.
((("something" "chases" "rabbit" "+") ("rabbit" "likes" "mouse" "+")) -> ("something" "likes" "dog" "+"))
If something needs the dog and it is not red then it does not like the dog.
((("something" "needs" "dog" "+") ("something" "is" "red" "~")) -> ("something" "likes" "dog" "-"))
The rabbit likes the mouse.
True
1
proof
[(triple8)]
("rabbit" "likes" "mouse" "+")
triple8
The tiger chases the dog.
False
1
inv-proof
[(triple10)]
("tiger" "chases" "dog" "+")
triple10
The dog chases the rabbit.
True
3
proof
[(((triple4 triple5) -> rule3))]
("dog" "chases" "rabbit" "+")
((triple4 triple5) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog does not chase the rabbit.
False
3
inv-proof
[(((triple4 triple5) -> rule3))]
("dog" "chases" "rabbit" "-")
((triple4 triple5) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog likes the dog.
True
5
proof
[(((((triple4 triple5) -> rule3) triple8) -> rule8))]
("dog" "likes" "dog" "+")
((((triple4 triple5) -> (rule3 % int2)) triple8) -> (rule8 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog does not like the dog.
False
5
inv-proof
[(((((triple4 triple5) -> rule3) triple8) -> rule8))]
("dog" "likes" "dog" "-")
((((triple4 triple5) -> (rule3 % int2)) triple8) -> (rule8 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog chases the tiger.
True
6
proof
[(((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5))]
("dog" "chases" "tiger" "+")
((((((triple4 triple5) -> (rule3 % int3)) triple8) -> (rule8 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The dog does not chase the tiger.
False
6
inv-proof
[(((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5))]
("dog" "chases" "tiger" "-")
((((((triple4 triple5) -> (rule3 % int3)) triple8) -> (rule8 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The tiger chases the rabbit.
True
7
proof
[(((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7))]
("tiger" "chases" "rabbit" "+")
((((((((triple4 triple5) -> (rule3 % int4)) triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The tiger does not chase the rabbit.
False
7
inv-proof
[(((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7))]
("tiger" "chases" "rabbit" "-")
((((((((triple4 triple5) -> (rule3 % int4)) triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The tiger likes the dog.
True
9
proof
[(((((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7) triple8) -> rule8))]
("tiger" "likes" "dog" "+")
((((((((((triple4 triple5) -> (rule3 % int5)) triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule8 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The dog likes the dog.
("dog" "likes" "dog" "+")
int4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int5
The tiger does not like the dog.
False
9
inv-proof
[(((((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7) triple8) -> rule8))]
("tiger" "likes" "dog" "-")
((((((((((triple4 triple5) -> (rule3 % int5)) triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule8 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The dog likes the dog.
("dog" "likes" "dog" "+")
int4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int5
The mouse is not blue.
Unknown
inv-rconc
[@1: The mouse is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "is" "blue" "-")
The mouse likes the dog.
Unknown
rconc
[@1: The mouse likes the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("mouse" "likes" "dog" "+")
The dog is not red.
Unknown
inv-rconc
[@1: The dog is red.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "is" "red" "-")
The rabbit likes the dog.
Unknown
rconc
[@1: The rabbit likes the dog.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("rabbit" "likes" "dog" "+")
The mouse does not chase the rabbit.
Unknown
inv-random
[@0: The mouse chases the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "rabbit" "-")
The rabbit needs the mouse.
Unknown
random
[@0: The rabbit needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "mouse" "+")
The mouse does not like the rabbit.
Unknown
inv-random
[@0: The mouse likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "likes" "rabbit" "-")
The rabbit needs the tiger.
Unknown
random
[@0: The rabbit needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "tiger" "+")
The mouse is not kind.
Unknown
inv-random
[@0: The mouse is kind.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "kind" "-")
The tiger likes the tiger.
Unknown
random
[@0: The tiger likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "tiger" "+")
The rabbit does not like the rabbit.
Unknown
inv-random
[@0: The rabbit likes the rabbit.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "likes" "rabbit" "-")
The rabbit chases the dog.
Unknown
random
[@0: The rabbit chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "chases" "dog" "+")
@0: The dog chases the mouse.[(triple1)] The dog is blue.[(triple2)] The dog needs the mouse.[(triple3)] The mouse needs the dog.[(triple4)] The mouse needs the rabbit.[(triple5)] The mouse needs the tiger.[(triple6)] The rabbit is not kind.[(triple7)] The rabbit likes the mouse.[(triple8)] The rabbit needs the dog.[(triple9)] The tiger does not chase the dog.[(triple10)] The tiger does not need the rabbit.[(triple16)] The tiger is cold.[(triple11)] The tiger is kind.[(triple12)] The tiger is red.[(triple13)] The tiger is rough.[(triple14)] The tiger needs the mouse.[(triple15)] @1: The dog chases the rabbit.[(((triple4 triple5) -> rule3))] @2: The dog likes the dog.[(((((triple4 triple5) -> rule3) triple8) -> rule8))] @3: The dog chases the tiger.[(((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5))] @4: The tiger chases the rabbit.[(((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7))] @5: The tiger likes the dog.[(((((((((((triple4 triple5) -> rule3) triple8) -> rule8)) -> rule5)) -> rule7) triple8) -> rule8))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog is blue.
("dog" "is" "blue" "+")
triple2
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple3
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple4
The mouse needs the rabbit.
("mouse" "needs" "rabbit" "+")
triple5
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple6
The rabbit is not kind.
("rabbit" "is" "kind" "-")
triple7
The rabbit likes the mouse.
("rabbit" "likes" "mouse" "+")
triple8
The rabbit needs the dog.
("rabbit" "needs" "dog" "+")
triple9
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
triple10
The tiger does not need the rabbit.
("tiger" "needs" "rabbit" "-")
triple16
The tiger is cold.
("tiger" "is" "cold" "+")
triple11
The tiger is kind.
("tiger" "is" "kind" "+")
triple12
The tiger is red.
("tiger" "is" "red" "+")
triple13
The tiger is rough.
("tiger" "is" "rough" "+")
triple14
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple15
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
((triple4 triple5) -> (rule3 % int1))
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
((((triple4 triple5) -> (rule3 % int2)) triple8) -> (rule8 % int1))
The dog likes the dog.
("dog" "likes" "dog" "+")
int1
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
((((((triple4 triple5) -> (rule3 % int3)) triple8) -> (rule8 % int2))) -> (rule5 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog likes the dog.
("dog" "likes" "dog" "+")
int2
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int3
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((((((((triple4 triple5) -> (rule3 % int4)) triple8) -> (rule8 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int2
The dog likes the dog.
("dog" "likes" "dog" "+")
int3
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int4
The tiger likes the dog.
("tiger" "likes" "dog" "+")
((((((((((triple4 triple5) -> (rule3 % int5)) triple8) -> (rule8 % int4))) -> (rule5 % int3))) -> (rule7 % int2)) triple8) -> (rule8 % int1))
The tiger likes the dog.
("tiger" "likes" "dog" "+")
int1
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int3
The dog likes the dog.
("dog" "likes" "dog" "+")
int4
The dog chases the rabbit.
("dog" "chases" "rabbit" "+")
int5