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