The cow is young. The cow visits the mouse. The lion is nice. The mouse is nice. The mouse does not see the lion. The mouse visits the cow. The mouse does not visit the lion. If something is nice then it chases the lion. If something chases the cow then it sees the mouse. If something is blue then it sees the mouse. If something sees the mouse then it sees the cow. If the cow is not red then the cow does not chase the lion. If something visits the mouse then it chases the cow.
The cow is young.
("cow" "is" "young" "+")
The cow visits the mouse.
("cow" "visits" "mouse" "+")
The lion is nice.
("lion" "is" "nice" "+")
The mouse is nice.
("mouse" "is" "nice" "+")
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
The mouse visits the cow.
("mouse" "visits" "cow" "+")
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
If something is nice then it chases the lion.
((("something" "is" "nice" "+")) -> ("something" "chases" "lion" "+"))
If something chases the cow then it sees the mouse.
((("something" "chases" "cow" "+")) -> ("something" "sees" "mouse" "+"))
If something is blue then it sees the mouse.
((("something" "is" "blue" "+")) -> ("something" "sees" "mouse" "+"))
If something sees the mouse then it sees the cow.
((("something" "sees" "mouse" "+")) -> ("something" "sees" "cow" "+"))
If the cow is not red then the cow does not chase the lion.
((("cow" "is" "red" "~")) -> ("cow" "chases" "lion" "-"))
If something visits the mouse then it chases the cow.
((("something" "visits" "mouse" "+")) -> ("something" "chases" "cow" "+"))
The mouse is nice.
True
1
proof
[(triple4)]
("mouse" "is" "nice" "+")
triple4
The mouse visits the lion.
False
1
inv-proof
[(triple7)]
("mouse" "visits" "lion" "+")
triple7
The cow chases the cow.
True
2
proof
[(((triple2) -> rule6))]
("cow" "chases" "cow" "+")
((triple2) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The mouse does not chase the lion.
False
2
inv-proof
[(((triple4) -> rule1))]
("mouse" "chases" "lion" "-")
((triple4) -> (rule1 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The cow sees the mouse.
True
3
proof
[(((((triple2) -> rule6)) -> rule2))]
("cow" "sees" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow does not see the mouse.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule2))]
("cow" "sees" "mouse" "-")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the cow.
True
4
proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("cow" "sees" "cow" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The cow does not see the cow.
False
4
inv-proof
[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
("cow" "sees" "cow" "-")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3
The lion does not chase the cow.
Unknown
inv-rconc
[@1: The lion chases the cow.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("lion" "chases" "cow" "-")
The lion sees the cow.
Unknown
rconc
[@3: The lion sees the cow.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule6 <- FAIL)]]
("lion" "sees" "cow" "+")
The lion does not see the mouse.
Unknown
inv-rconc
[@2: The lion sees the mouse.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("lion" "sees" "mouse" "-")
The mouse sees the mouse.
Unknown
rconc
[@2: The mouse sees the mouse.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("mouse" "sees" "mouse" "+")
The cow does not visit the lion.
Unknown
inv-random
[@0: The cow visits the lion.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "lion" "-")
The cow visits the cow.
Unknown
random
[@0: The cow visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "cow" "+")
The lion does not visit the cow.
Unknown
inv-random
[@0: The lion visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("lion" "visits" "cow" "-")
The cow is blue.
Unknown
random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "+")
@0: The cow is young.[(triple1)] The cow visits the mouse.[(triple2)] The lion is nice.[(triple3)] The mouse does not see the lion.[(triple5)] The mouse does not visit the lion.[(triple7)] The mouse is nice.[(triple4)] The mouse visits the cow.[(triple6)] @1: The cow chases the cow.[(((triple2) -> rule6))] The lion chases the lion.[(((triple3) -> rule1))] The mouse chases the lion.[(((triple4) -> rule1))] @2: The cow sees the mouse.[(((((triple2) -> rule6)) -> rule2))] @3: The cow sees the cow.[(((((((triple2) -> rule6)) -> rule2)) -> rule4))]
The cow is young.
("cow" "is" "young" "+")
triple1
The cow visits the mouse.
("cow" "visits" "mouse" "+")
triple2
The lion is nice.
("lion" "is" "nice" "+")
triple3
The mouse does not see the lion.
("mouse" "sees" "lion" "-")
triple5
The mouse does not visit the lion.
("mouse" "visits" "lion" "-")
triple7
The mouse is nice.
("mouse" "is" "nice" "+")
triple4
The mouse visits the cow.
("mouse" "visits" "cow" "+")
triple6
The cow chases the cow.
("cow" "chases" "cow" "+")
((triple2) -> (rule6 % int1))
The cow chases the cow.
("cow" "chases" "cow" "+")
int1
The lion chases the lion.
("lion" "chases" "lion" "+")
((triple3) -> (rule1 % int1))
The lion chases the lion.
("lion" "chases" "lion" "+")
int1
The mouse chases the lion.
("mouse" "chases" "lion" "+")
((triple4) -> (rule1 % int1))
The mouse chases the lion.
("mouse" "chases" "lion" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int1
The cow chases the cow.
("cow" "chases" "cow" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow sees the mouse.
("cow" "sees" "mouse" "+")
int2
The cow chases the cow.
("cow" "chases" "cow" "+")
int3