The cat does not chase the cow. The cat chases the tiger. The cat is kind. The cow chases the cat. The cow is kind. The cow visits the mouse. The mouse is green. The mouse visits the cat. The tiger chases the mouse. The tiger sees the cat. If something is kind and it visits the cat then it does not visit the tiger. If the mouse visits the cow then the cow is green. If the cat visits the tiger then the tiger chases the cow. If the cow visits the mouse and the cow chases the mouse then the cow chases the cat. If something chases the tiger then it is cold. If something visits the mouse then it visits the cat. If something is cold then it visits the cat. If the tiger chases the cow and the cow chases the mouse then the tiger does not see the mouse.
The cat does not chase the cow.
("cat" "chases" "cow" "-")
The cat chases the tiger.
("cat" "chases" "tiger" "+")
The cat is kind.
("cat" "is" "kind" "+")
The cow chases the cat.
("cow" "chases" "cat" "+")
The cow is kind.
("cow" "is" "kind" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The mouse is green.
("mouse" "is" "green" "+")
The mouse visits the cat.
("mouse" "visits" "cat" "+")
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
The tiger sees the cat.
("tiger" "sees" "cat" "+")
If something is kind and it visits the cat then it does not visit the tiger.
((("something" "is" "kind" "+") ("something" "visits" "cat" "+")) -> ("something" "visits" "tiger" "-"))
If the mouse visits the cow then the cow is green.
((("mouse" "visits" "cow" "+")) -> ("cow" "is" "green" "+"))
If the cat visits the tiger then the tiger chases the cow.
((("cat" "visits" "tiger" "+")) -> ("tiger" "chases" "cow" "+"))
If the cow visits the mouse and the cow chases the mouse then the cow chases the cat.
((("cow" "visits" "mouse" "+") ("cow" "chases" "mouse" "+")) -> ("cow" "chases" "cat" "+"))
If something chases the tiger then it is cold.
((("something" "chases" "tiger" "+")) -> ("something" "is" "cold" "+"))
If something visits the mouse then it visits the cat.
((("something" "visits" "mouse" "+")) -> ("something" "visits" "cat" "+"))
If something is cold then it visits the cat.
((("something" "is" "cold" "+")) -> ("something" "visits" "cat" "+"))
If the tiger chases the cow and the cow chases the mouse then the tiger does not see the mouse.
((("tiger" "chases" "cow" "+") ("cow" "chases" "mouse" "+")) -> ("tiger" "sees" "mouse" "-"))
The cat does not chase the cow.
True
1
proof
[(triple1)]
("cat" "chases" "cow" "-")
triple1
The cat chases the cow.
False
1
inv-proof
[(triple1)]
("cat" "chases" "cow" "+")
triple1
The cow visits the cat.
True
2
proof
[(((triple6) -> rule6))]
("cow" "visits" "cat" "+")
((triple6) -> (rule6 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow does not visit the cat.
False
2
inv-proof
[(((triple6) -> rule6))]
("cow" "visits" "cat" "-")
((triple6) -> (rule6 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cow does not visit the tiger.
True
4
proof
[(((triple5 ((triple6) -> rule6)) -> rule1))]
("cow" "visits" "tiger" "-")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cow visits the tiger.
False
4
inv-proof
[(((triple5 ((triple6) -> rule6)) -> rule1))]
("cow" "visits" "tiger" "+")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat does not visit the tiger.
True
5
proof
[(((triple3 ((((triple2) -> rule5)) -> rule7)) -> rule1))]
("cat" "visits" "tiger" "-")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The cat visits the tiger.
False
5
inv-proof
[(((triple3 ((((triple2) -> rule5)) -> rule7)) -> rule1))]
("cat" "visits" "tiger" "+")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3
The tiger does not visit the cat.
Unknown
inv-rconc
[@2: The tiger visits the cat.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("tiger" "visits" "cat" "-")
The cow is green.
Unknown
rconc
[@1: The cow is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "green" "+")
The mouse is not cold.
Unknown
inv-rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "cold" "-")
The cow is cold.
Unknown
rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cow" "is" "cold" "+")
The tiger does not chase the tiger.
Unknown
inv-random
[@0: The tiger chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "tiger" "-")
The cow chases the tiger.
Unknown
random
[@0: The cow chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "tiger" "+")
The mouse does not chase the tiger.
Unknown
inv-random
[@0: The mouse chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "chases" "tiger" "-")
The cow sees the cat.
Unknown
random
[@0: The cow sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cat" "+")
@0: The cat chases the tiger.[(triple2)] The cat does not chase the cow.[(triple1)] The cat is kind.[(triple3)] The cow chases the cat.[(triple4)] The cow is kind.[(triple5)] The cow visits the mouse.[(triple6)] The mouse is green.[(triple7)] The mouse visits the cat.[(triple8)] The tiger chases the mouse.[(triple9)] The tiger sees the cat.[(triple10)] @1: The cat is cold.[(((triple2) -> rule5))] The cow visits the cat.[(((triple6) -> rule6))] @2: The cat visits the cat.[(((((triple2) -> rule5)) -> rule7))] The cow does not visit the tiger.[(((triple5 ((triple6) -> rule6)) -> rule1))] @3: The cat does not visit the tiger.[(((triple3 ((((triple2) -> rule5)) -> rule7)) -> rule1))]
The cat chases the tiger.
("cat" "chases" "tiger" "+")
triple2
The cat does not chase the cow.
("cat" "chases" "cow" "-")
triple1
The cat is kind.
("cat" "is" "kind" "+")
triple3
The cow chases the cat.
("cow" "chases" "cat" "+")
triple4
The cow is kind.
("cow" "is" "kind" "+")
triple5
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple6
The mouse is green.
("mouse" "is" "green" "+")
triple7
The mouse visits the cat.
("mouse" "visits" "cat" "+")
triple8
The tiger chases the mouse.
("tiger" "chases" "mouse" "+")
triple9
The tiger sees the cat.
("tiger" "sees" "cat" "+")
triple10
The cat is cold.
("cat" "is" "cold" "+")
((triple2) -> (rule5 % int1))
The cat is cold.
("cat" "is" "cold" "+")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
((triple6) -> (rule6 % int1))
The cow visits the cat.
("cow" "visits" "cat" "+")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
((((triple2) -> (rule5 % int2))) -> (rule7 % int1))
The cat visits the cat.
("cat" "visits" "cat" "+")
int1
The cat is cold.
("cat" "is" "cold" "+")
int2
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
((triple5 ((triple6) -> (rule6 % int2))) -> (rule1 % int1))
The cow does not visit the tiger.
("cow" "visits" "tiger" "-")
int1
The cow visits the cat.
("cow" "visits" "cat" "+")
int2
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
((triple3 ((((triple2) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule1 % int1))
The cat does not visit the tiger.
("cat" "visits" "tiger" "-")
int1
The cat visits the cat.
("cat" "visits" "cat" "+")
int2
The cat is cold.
("cat" "is" "cold" "+")
int3