The cat chases the tiger. The cow chases the cat. The mouse visits the tiger. The tiger is green. If something is green then it chases the tiger. If something chases the mouse and it is rough then the mouse is not rough. If something visits the mouse and it visits the cow then the mouse does not need the tiger. If the cow visits the mouse and the cow is round then the mouse does not need the tiger. If something is green then it is not nice. If something chases the tiger then it visits the tiger.
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
The tiger is green.
("tiger" "is" "green" "+")
If something is green then it chases the tiger.
((("something" "is" "green" "+")) -> ("something" "chases" "tiger" "+"))
If something chases the mouse and it is rough then the mouse is not rough.
((("something" "chases" "mouse" "+") ("something" "is" "rough" "+")) -> ("mouse" "is" "rough" "-"))
If something visits the mouse and it visits the cow then the mouse does not need the tiger.
((("something" "visits" "mouse" "+") ("something" "visits" "cow" "+")) -> ("mouse" "needs" "tiger" "-"))
If the cow visits the mouse and the cow is round then the mouse does not need the tiger.
((("cow" "visits" "mouse" "+") ("cow" "is" "round" "+")) -> ("mouse" "needs" "tiger" "-"))
If something is green then it is not nice.
((("something" "is" "green" "+")) -> ("something" "is" "nice" "-"))
If something chases the tiger then it visits the tiger.
((("something" "chases" "tiger" "+")) -> ("something" "visits" "tiger" "+"))
The mouse visits the tiger.
True
1
proof
[(triple3)]
("mouse" "visits" "tiger" "+")
triple3
The cow does not chase the cat.
False
1
inv-proof
[(triple2)]
("cow" "chases" "cat" "-")
triple2
The tiger chases the tiger.
True
2
proof
[(((triple4) -> rule1))]
("tiger" "chases" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is nice.
False
2
inv-proof
[(((triple4) -> rule5))]
("tiger" "is" "nice" "+")
((triple4) -> (rule5 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger visits the tiger.
True
3
proof
[(((((triple4) -> rule1)) -> rule6))]
("tiger" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The tiger does not visit the tiger.
False
3
inv-proof
[(((((triple4) -> rule1)) -> rule6))]
("tiger" "visits" "tiger" "-")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2
The cow does not chase the tiger.
Unknown
inv-rconc
[@1: The cow chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "chases" "tiger" "-")
The mouse chases the tiger.
Unknown
rconc
[@1: The mouse chases the tiger.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "chases" "tiger" "+")
The cow does not visit the tiger.
Unknown
inv-rconc
[@2: The cow visits the tiger.[CWA. Example of deepest failure = (rule6 <- rule1 <- FAIL)]]
("cow" "visits" "tiger" "-")
The cow needs the mouse.
Unknown
random
[@0: The cow needs the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "needs" "mouse" "+")
The cat is not rough.
Unknown
inv-random
[@0: The cat is rough.[CWA. Example of deepest failure = (FAIL)]]
("cat" "is" "rough" "-")
The cat needs the tiger.
Unknown
random
[@0: The cat needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cat" "needs" "tiger" "+")
@0: The cat chases the tiger.[(triple1)] The cow chases the cat.[(triple2)] The mouse visits the tiger.[(triple3)] The tiger is green.[(triple4)] @1: The cat visits the tiger.[(((triple1) -> rule6))] The tiger chases the tiger.[(((triple4) -> rule1))] The tiger is not nice.[(((triple4) -> rule5))] @2: The tiger visits the tiger.[(((((triple4) -> rule1)) -> rule6))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple1
The cow chases the cat.
("cow" "chases" "cat" "+")
triple2
The mouse visits the tiger.
("mouse" "visits" "tiger" "+")
triple3
The tiger is green.
("tiger" "is" "green" "+")
triple4
The cat visits the tiger.
("cat" "visits" "tiger" "+")
((triple1) -> (rule6 % int1))
The cat visits the tiger.
("cat" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
((triple4) -> (rule1 % int1))
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int1
The tiger is not nice.
("tiger" "is" "nice" "-")
((triple4) -> (rule5 % int1))
The tiger is not nice.
("tiger" "is" "nice" "-")
int1
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((triple4) -> (rule1 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger chases the tiger.
("tiger" "chases" "tiger" "+")
int2