The cow chases the tiger. The dog sees the cow. The mouse needs the dog. The tiger needs the dog. If something is young and it chases the dog then it chases the tiger. If something needs the mouse and the mouse chases the tiger then it is cold. If something chases the cow then the cow chases the mouse. If something sees the tiger then the tiger chases the mouse. If something chases the tiger then the tiger chases the dog. All nice things are big. All round things are nice. If something needs the cow and it is round then the cow sees the tiger.
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse needs the dog.
("mouse" "needs" "dog" "+")
The tiger needs the dog.
("tiger" "needs" "dog" "+")
If something is young and it chases the dog then it chases the tiger.
((("something" "is" "young" "+") ("something" "chases" "dog" "+")) -> ("something" "chases" "tiger" "+"))
If something needs the mouse and the mouse chases the tiger then it is cold.
((("something" "needs" "mouse" "+") ("mouse" "chases" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something chases the cow then the cow chases the mouse.
((("something" "chases" "cow" "+")) -> ("cow" "chases" "mouse" "+"))
If something sees the tiger then the tiger chases the mouse.
((("something" "sees" "tiger" "+")) -> ("tiger" "chases" "mouse" "+"))
If something chases the tiger then the tiger chases the dog.
((("something" "chases" "tiger" "+")) -> ("tiger" "chases" "dog" "+"))
All nice things are big.
((("something" "is" "nice" "+")) -> ("something" "is" "big" "+"))
All round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If something needs the cow and it is round then the cow sees the tiger.
((("something" "needs" "cow" "+") ("something" "is" "round" "+")) -> ("cow" "sees" "tiger" "+"))
The mouse needs the dog.
True
1
proof
[(triple3)]
("mouse" "needs" "dog" "+")
triple3
The tiger does not need the dog.
False
1
inv-proof
[(triple4)]
("tiger" "needs" "dog" "-")
triple4
The tiger chases the dog.
True
2
proof
[(((triple1) -> rule5))]
("tiger" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The tiger does not chase the dog.
False
2
inv-proof
[(((triple1) -> rule5))]
("tiger" "chases" "dog" "-")
((triple1) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1
The cow does not see the tiger.
Unknown
inv-rconc
[@1: The cow sees the tiger.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("cow" "sees" "tiger" "-")
The dog chases the tiger.
Unknown
rconc
[@1: The dog chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "chases" "tiger" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
@0: The cow chases the tiger.[(triple1)] The dog sees the cow.[(triple2)] The mouse needs the dog.[(triple3)] The tiger needs the dog.[(triple4)] @1: The tiger chases the dog.[(((triple1) -> rule5))]
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple1
The dog sees the cow.
("dog" "sees" "cow" "+")
triple2
The mouse needs the dog.
("mouse" "needs" "dog" "+")
triple3
The tiger needs the dog.
("tiger" "needs" "dog" "+")
triple4
The tiger chases the dog.
("tiger" "chases" "dog" "+")
((triple1) -> (rule5 % int1))
The tiger chases the dog.
("tiger" "chases" "dog" "+")
int1