The dog chases the tiger. The dog eats the tiger. The dog is nice. The dog visits the rabbit. The dog visits the tiger. The mouse is big. The mouse visits the dog. The rabbit chases the dog. The rabbit chases the mouse. The rabbit is nice. The tiger chases the mouse. The tiger eats the rabbit. If the tiger chases the mouse then the tiger chases the rabbit. If something eats the rabbit and it is big then it is cold.
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The mouse is big.
("mouse" "is" "big" "+")
The mouse visits the dog.
("mouse" "visits" "dog" "+")
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
The rabbit is nice.
("rabbit" "is" "nice" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
If the tiger chases the mouse then the tiger chases the rabbit.
((("tiger" "chases" "mouse" "+")) -> ("tiger" "chases" "rabbit" "+"))
If something eats the rabbit and it is big then it is cold.
((("something" "eats" "rabbit" "+") ("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
The dog eats the tiger.
True
1
proof
[(triple2)]
("dog" "eats" "tiger" "+")
triple2
The tiger does not chase the mouse.
False
1
inv-proof
[(triple11)]
("tiger" "chases" "mouse" "-")
triple11
The tiger chases the rabbit.
True
2
proof
[(((triple11) -> rule1))]
("tiger" "chases" "rabbit" "+")
((triple11) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger does not chase the rabbit.
False
2
inv-proof
[(((triple11) -> rule1))]
("tiger" "chases" "rabbit" "-")
((triple11) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1
The tiger is not cold.
Unknown
inv-rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "cold" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "is" "cold" "+")
The rabbit does not eat the mouse.
Unknown
inv-random
[@0: The rabbit eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "eats" "mouse" "-")
The mouse eats the tiger.
Unknown
random
[@0: The mouse eats the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "tiger" "+")
@0: The dog chases the tiger.[(triple1)] The dog eats the tiger.[(triple2)] The dog is nice.[(triple3)] The dog visits the rabbit.[(triple4)] The dog visits the tiger.[(triple5)] The mouse is big.[(triple6)] The mouse visits the dog.[(triple7)] The rabbit chases the dog.[(triple8)] The rabbit chases the mouse.[(triple9)] The rabbit is nice.[(triple10)] The tiger chases the mouse.[(triple11)] The tiger eats the rabbit.[(triple12)] @1: The tiger chases the rabbit.[(((triple11) -> rule1))]
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog is nice.
("dog" "is" "nice" "+")
triple3
The dog visits the rabbit.
("dog" "visits" "rabbit" "+")
triple4
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple5
The mouse is big.
("mouse" "is" "big" "+")
triple6
The mouse visits the dog.
("mouse" "visits" "dog" "+")
triple7
The rabbit chases the dog.
("rabbit" "chases" "dog" "+")
triple8
The rabbit chases the mouse.
("rabbit" "chases" "mouse" "+")
triple9
The rabbit is nice.
("rabbit" "is" "nice" "+")
triple10
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple11
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
triple12
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
((triple11) -> (rule1 % int1))
The tiger chases the rabbit.
("tiger" "chases" "rabbit" "+")
int1