The dog chases the mouse. The dog eats the tiger. The dog is young. The mouse is round. The mouse is young. The tiger is round. The tiger visits the mouse. If someone visits the dog then they visit the mouse. If someone chases the dog and the dog chases the mouse then they chase the tiger. If someone eats the mouse then the mouse chases the tiger. If someone eats the mouse then the mouse chases the dog. If someone chases the mouse and the mouse is young then the mouse eats the dog. If the dog is young then the dog eats the mouse. All nice people are young. If someone is cold then they eat the tiger.
The dog chases the mouse.
("dog" "chases" "mouse" "+")
The dog eats the tiger.
("dog" "eats" "tiger" "+")
The dog is young.
("dog" "is" "young" "+")
The mouse is round.
("mouse" "is" "round" "+")
The mouse is young.
("mouse" "is" "young" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone visits the dog then they visit the mouse.
((("someone" "visits" "dog" "+")) -> ("someone" "visits" "mouse" "+"))
If someone chases the dog and the dog chases the mouse then they chase the tiger.
((("someone" "chases" "dog" "+") ("dog" "chases" "mouse" "+")) -> ("someone" "chases" "tiger" "+"))
If someone eats the mouse then the mouse chases the tiger.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "tiger" "+"))
If someone eats the mouse then the mouse chases the dog.
((("someone" "eats" "mouse" "+")) -> ("mouse" "chases" "dog" "+"))
If someone chases the mouse and the mouse is young then the mouse eats the dog.
((("someone" "chases" "mouse" "+") ("mouse" "is" "young" "+")) -> ("mouse" "eats" "dog" "+"))
If the dog is young then the dog eats the mouse.
((("dog" "is" "young" "+")) -> ("dog" "eats" "mouse" "+"))
All nice people are young.
((("someone" "is" "nice" "+")) -> ("someone" "is" "young" "+"))
If someone is cold then they eat the tiger.
((("someone" "is" "cold" "+")) -> ("someone" "eats" "tiger" "+"))
The mouse is young.
True
1
proof
[(triple5)]
("mouse" "is" "young" "+")
triple5
The tiger is not round.
False
1
inv-proof
[(triple6)]
("tiger" "is" "round" "-")
triple6
The dog does not chase the tiger.
Unknown
inv-rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("dog" "chases" "tiger" "-")
The tiger visits the tiger.
Unknown
random
[@0: The tiger visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "tiger" "+")
@0: The dog chases the mouse.[(triple1)] The dog eats the tiger.[(triple2)] The dog is young.[(triple3)] The mouse is round.[(triple4)] The mouse is young.[(triple5)] The tiger is round.[(triple6)] The tiger visits the mouse.[(triple7)] @1: The dog eats the mouse.[(((triple3) -> rule6))] The mouse eats the dog.[(((triple1 triple5) -> rule5))] @2: The mouse chases the dog.[(((((triple3) -> rule6)) -> rule4))] The mouse chases the tiger.[(((((triple3) -> rule6)) -> rule3) OR ((((((triple3) -> rule6)) -> rule4) triple1) -> rule2))]
The dog chases the mouse.
("dog" "chases" "mouse" "+")
triple1
The dog eats the tiger.
("dog" "eats" "tiger" "+")
triple2
The dog is young.
("dog" "is" "young" "+")
triple3
The mouse is round.
("mouse" "is" "round" "+")
triple4
The mouse is young.
("mouse" "is" "young" "+")
triple5
The tiger is round.
("tiger" "is" "round" "+")
triple6
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple7
The dog eats the mouse.
("dog" "eats" "mouse" "+")
((triple3) -> (rule6 % int1))
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int1
The mouse eats the dog.
("mouse" "eats" "dog" "+")
((triple1 triple5) -> (rule5 % int1))
The mouse eats the dog.
("mouse" "eats" "dog" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
((((triple3) -> (rule6 % int2))) -> (rule4 % int1))
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
((((triple3) -> (rule6 % int2))) -> (rule3 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int2
((((((triple3) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule2 % int1))
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
int1
The mouse chases the dog.
("mouse" "chases" "dog" "+")
int2
The dog eats the mouse.
("dog" "eats" "mouse" "+")
int3