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