The cow is green. The cow likes the dog. The dog chases the tiger. The dog sees the cow. The mouse chases the tiger. The mouse is not big. The tiger sees the mouse. If the cow chases the tiger then the cow is round. If something is green then it sees the cow. If something sees the tiger and it likes the mouse then the mouse is big. If something sees the cow then it chases the tiger. If something sees the mouse then it does not chase the dog. If something chases the mouse and it is not green then it is big. If something chases the mouse and the mouse chases the dog then the mouse likes the cow. If something likes the cow and the cow does not chase the dog then the cow is not blue.
The cow is green.
("cow" "is" "green" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
The mouse is not big.
("mouse" "is" "big" "-")
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
If the cow chases the tiger then the cow is round.
((("cow" "chases" "tiger" "+")) -> ("cow" "is" "round" "+"))
If something is green then it sees the cow.
((("something" "is" "green" "+")) -> ("something" "sees" "cow" "+"))
If something sees the tiger and it likes the mouse then the mouse is big.
((("something" "sees" "tiger" "+") ("something" "likes" "mouse" "+")) -> ("mouse" "is" "big" "+"))
If something sees the cow then it chases the tiger.
((("something" "sees" "cow" "+")) -> ("something" "chases" "tiger" "+"))
If something sees the mouse then it does not chase the dog.
((("something" "sees" "mouse" "+")) -> ("something" "chases" "dog" "-"))
If something chases the mouse and it is not green then it is big.
((("something" "chases" "mouse" "+") ("something" "is" "green" "~")) -> ("something" "is" "big" "+"))
If something chases the mouse and the mouse chases the dog then the mouse likes the cow.
((("something" "chases" "mouse" "+") ("mouse" "chases" "dog" "+")) -> ("mouse" "likes" "cow" "+"))
If something likes the cow and the cow does not chase the dog then the cow is not blue.
((("something" "likes" "cow" "+") ("cow" "chases" "dog" "~")) -> ("cow" "is" "blue" "-"))
The cow likes the dog.
True
1
proof
[(triple2)]
("cow" "likes" "dog" "+")
triple2
The mouse is big.
False
1
inv-proof
[(triple6)]
("mouse" "is" "big" "+")
triple6
The cow sees the cow.
True
2
proof
[(((triple1) -> rule2))]
("cow" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple1) -> rule2))]
("cow" "sees" "cow" "-")
((triple1) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow chases the tiger.
True
3
proof
[(((((triple1) -> rule2)) -> rule4))]
("cow" "chases" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow does not chase the tiger.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule4))]
("cow" "chases" "tiger" "-")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The mouse does not see the cow.
Unknown
inv-rconc
[@1: The mouse sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "cow" "-")
The tiger sees the cow.
Unknown
rconc
[@1: The tiger sees the cow.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "sees" "cow" "+")
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("tiger" "is" "big" "-")
The tiger likes the cow.
Unknown
random
[@0: The tiger likes the cow.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "likes" "cow" "+")
The mouse does not see the mouse.
Unknown
inv-random
[@0: The mouse sees the mouse.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "mouse" "-")
The tiger sees the tiger.
Unknown
random
[@0: The tiger sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "tiger" "+")
@0: The cow is green.[(triple1)] The cow likes the dog.[(triple2)] The dog chases the tiger.[(triple3 OR ((triple4) -> rule4))] The dog sees the cow.[(triple4)] The mouse chases the tiger.[(triple5)] The mouse is not big.[(triple6)] The tiger sees the mouse.[(triple7)] @1: The cow sees the cow.[(((triple1) -> rule2))] The tiger does not chase the dog.[(((triple7) -> rule5))] @2: The cow chases the tiger.[(((((triple1) -> rule2)) -> rule4))] @3: The cow is round.[(((((((triple1) -> rule2)) -> rule4)) -> rule1))]
The cow is green.
("cow" "is" "green" "+")
triple1
The cow likes the dog.
("cow" "likes" "dog" "+")
triple2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple3
((triple4) -> (rule4 % int1))
The dog chases the tiger.
("dog" "chases" "tiger" "+")
int1
The dog sees the cow.
("dog" "sees" "cow" "+")
triple4
The mouse chases the tiger.
("mouse" "chases" "tiger" "+")
triple5
The mouse is not big.
("mouse" "is" "big" "-")
triple6
The tiger sees the mouse.
("tiger" "sees" "mouse" "+")
triple7
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple1) -> (rule2 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
((triple7) -> (rule5 % int1))
The tiger does not chase the dog.
("tiger" "chases" "dog" "-")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
((((triple1) -> (rule2 % int2))) -> (rule4 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow sees the cow.
("cow" "sees" "cow" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((((triple1) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule1 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int2
The cow sees the cow.
("cow" "sees" "cow" "+")
int3