The cat chases the mouse. The cat eats the dog. The cat needs the dog. The dog chases the mouse. The dog is green. The dog is rough. The dog needs the mouse. The mouse chases the dog. The mouse eats the tiger. The mouse is not young. The mouse needs the tiger. The tiger chases the dog. The tiger does not eat the cat. The tiger is round. The tiger is young. The tiger needs the mouse. If something is round then it chases the tiger. If something eats the dog then the dog is young. If something eats the tiger and it does not eat the dog then the dog eats the cat. If something is young then it chases the cat. If the cat chases the dog then the cat eats the tiger. If something needs the mouse and the mouse does not eat the cat then it needs the dog. If something chases the dog then it does not chase the mouse. If something eats the mouse then the mouse chases the dog.
The cat chases the mouse.
("cat" "chases" "mouse" "+")
The cat eats the dog.
("cat" "eats" "dog" "+")
The cat needs the dog.
("cat" "needs" "dog" "+")
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is rough.
("dog" "is" "rough" "+")
The dog needs the mouse.
("dog" "needs" "mouse" "+")
The mouse chases the dog.
("mouse" "chases" "dog" "+")
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
The mouse is not young.
("mouse" "is" "young" "-")
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
The tiger chases the dog.
("tiger" "chases" "dog" "+")
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
The tiger is round.
("tiger" "is" "round" "+")
The tiger is young.
("tiger" "is" "young" "+")
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
If something is round then it chases the tiger.
((("something" "is" "round" "+")) -> ("something" "chases" "tiger" "+"))
If something eats the dog then the dog is young.
((("something" "eats" "dog" "+")) -> ("dog" "is" "young" "+"))
If something eats the tiger and it does not eat the dog then the dog eats the cat.
((("something" "eats" "tiger" "+") ("something" "eats" "dog" "~")) -> ("dog" "eats" "cat" "+"))
If something is young then it chases the cat.
((("something" "is" "young" "+")) -> ("something" "chases" "cat" "+"))
If the cat chases the dog then the cat eats the tiger.
((("cat" "chases" "dog" "+")) -> ("cat" "eats" "tiger" "+"))
If something needs the mouse and the mouse does not eat the cat then it needs the dog.
((("something" "needs" "mouse" "+") ("mouse" "eats" "cat" "~")) -> ("something" "needs" "dog" "+"))
If something chases the dog then it does not chase the mouse.
((("something" "chases" "dog" "+")) -> ("something" "chases" "mouse" "-"))
If something eats the mouse then the mouse chases the dog.
((("something" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
The mouse eats the tiger.
True
1
proof
[(triple9)]
("mouse" "eats" "tiger" "+")
triple9
The mouse does not eat the tiger.
False
1
inv-proof
[(triple9)]
("mouse" "eats" "tiger" "-")
triple9
The tiger does not chase the mouse.
True
2
proof
[(((triple12) -> rule7))]
("tiger" "chases" "mouse" "-")
((triple12) -> (rule7 % int1))
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int1
The mouse chases the mouse.
False
2
inv-proof
[(((triple8) -> rule7))]
("mouse" "chases" "mouse" "+")
((triple8) -> (rule7 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The cat does not chase the cat.
Unknown
inv-rconc
[@1: The cat chases the cat.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "chases" "cat" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "tiger" "+")
The mouse does not eat the mouse.
Unknown
inv-random
[@0: The mouse eats the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "eats" "mouse" "-")
The tiger is green.
Unknown
random
[@0: The tiger is green.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "green" "+")
@0: The cat chases the mouse.[(triple1)] The cat eats the dog.[(triple2)] The cat needs the dog.[(triple3)] The dog chases the mouse.[(triple4)] The dog is green.[(triple5)] The dog is rough.[(triple6)] The dog needs the mouse.[(triple7)] The mouse chases the dog.[(triple8)] The mouse eats the tiger.[(triple9)] The mouse is not young.[(triple10)] The mouse needs the tiger.[(triple11)] The tiger chases the dog.[(triple12)] The tiger does not eat the cat.[(triple13)] The tiger is round.[(triple14)] The tiger is young.[(triple15)] The tiger needs the mouse.[(triple16)] @1: The dog is young.[(((triple2) -> rule2))] The mouse does not chase the mouse.[(((triple8) -> rule7))] The tiger chases the cat.[(((triple15) -> rule4))] The tiger chases the tiger.[(((triple14) -> rule1))] The tiger does not chase the mouse.[(((triple12) -> rule7))] @2: The dog chases the cat.[(((((triple2) -> rule2)) -> rule4))]
The cat chases the mouse.
("cat" "chases" "mouse" "+")
triple1
The cat eats the dog.
("cat" "eats" "dog" "+")
triple2
The cat needs the dog.
("cat" "needs" "dog" "+")
triple3
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog is rough.
("dog" "is" "rough" "+")
triple6
The dog needs the mouse.
("dog" "needs" "mouse" "+")
triple7
The mouse chases the dog.
("mouse" "chases" "dog" "+")
triple8
The mouse eats the tiger.
("mouse" "eats" "tiger" "+")
triple9
The mouse is not young.
("mouse" "is" "young" "-")
triple10
The mouse needs the tiger.
("mouse" "needs" "tiger" "+")
triple11
The tiger chases the dog.
("tiger" "chases" "dog" "+")
triple12
The tiger does not eat the cat.
("tiger" "eats" "cat" "-")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger is young.
("tiger" "is" "young" "+")
triple15
The tiger needs the mouse.
("tiger" "needs" "mouse" "+")
triple16
The dog is young.
("dog" "is" "young" "+")
((triple2) -> (rule2 % int1))
The dog is young.
("dog" "is" "young" "+")
int1
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
((triple8) -> (rule7 % int1))
The mouse does not chase the mouse.
("mouse" "chases" "mouse" "-")
int1
The tiger chases the cat.
("tiger" "chases" "cat" "+")
((triple15) -> (rule4 % int1))
The tiger chases the cat.
("tiger" "chases" "cat" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple14) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
((triple12) -> (rule7 % int1))
The tiger does not chase the mouse.
("tiger" "chases" "mouse" "-")
int1
The dog chases the cat.
("dog" "chases" "cat" "+")
((((triple2) -> (rule2 % int2))) -> (rule4 % int1))
The dog chases the cat.
("dog" "chases" "cat" "+")
int1
The dog is young.
("dog" "is" "young" "+")
int2