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