The cat visits the mouse. The cow is young. The cow sees the tiger. The mouse chases the cat. The mouse is young. The mouse sees the cat. The mouse sees the cow. The mouse does not visit the cow. The tiger visits the cow. The tiger visits the mouse. If someone is rough and they chase the mouse then they are cold. If the cow is rough and the cow is young then the cow is red. If someone is red then they chase the mouse. All cold people are red. If someone sees the cow then the cow is cold. If someone visits the mouse and the mouse chases the tiger then the mouse sees the tiger. If someone chases the mouse then the mouse is red.
The cat visits the mouse.
("cat" "visits" "mouse" "+")
The cow is young.
("cow" "is" "young" "+")
The cow sees the tiger.
("cow" "sees" "tiger" "+")
The mouse chases the cat.
("mouse" "chases" "cat" "+")
The mouse is young.
("mouse" "is" "young" "+")
The mouse sees the cat.
("mouse" "sees" "cat" "+")
The mouse sees the cow.
("mouse" "sees" "cow" "+")
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If someone is rough and they chase the mouse then they are cold.
((("someone" "is" "rough" "+") ("someone" "chases" "mouse" "+")) -> ("someone" "is" "cold" "+"))
If the cow is rough and the cow is young then the cow is red.
((("cow" "is" "rough" "+") ("cow" "is" "young" "+")) -> ("cow" "is" "red" "+"))
If someone is red then they chase the mouse.
((("someone" "is" "red" "+")) -> ("someone" "chases" "mouse" "+"))
All cold people are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
If someone sees the cow then the cow is cold.
((("someone" "sees" "cow" "+")) -> ("cow" "is" "cold" "+"))
If someone visits the mouse and the mouse chases the tiger then the mouse sees the tiger.
((("someone" "visits" "mouse" "+") ("mouse" "chases" "tiger" "+")) -> ("mouse" "sees" "tiger" "+"))
If someone chases the mouse then the mouse is red.
((("someone" "chases" "mouse" "+")) -> ("mouse" "is" "red" "+"))
The cat visits the mouse.
True
1
proof
[(triple1)]
("cat" "visits" "mouse" "+")
triple1
The tiger does not visit the cow.
False
1
inv-proof
[(triple9)]
("tiger" "visits" "cow" "-")
triple9
The cow is cold.
True
2
proof
[(((triple7) -> rule5))]
("cow" "is" "cold" "+")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple7) -> rule5))]
("cow" "is" "cold" "-")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
True
3
proof
[(((((triple7) -> rule5)) -> rule4))]
("cow" "is" "red" "+")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow is not red.
False
3
inv-proof
[(((((triple7) -> rule5)) -> rule4))]
("cow" "is" "red" "-")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow chases the mouse.
True
4
proof
[(((((((triple7) -> rule5)) -> rule4)) -> rule3))]
("cow" "chases" "mouse" "+")
((((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The cow does not chase the mouse.
False
4
inv-proof
[(((((((triple7) -> rule5)) -> rule4)) -> rule3))]
("cow" "chases" "mouse" "-")
((((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The mouse is red.
True
5
proof
[(((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7))]
("mouse" "is" "red" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The mouse is not red.
False
5
inv-proof
[(((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7))]
("mouse" "is" "red" "-")
((((((((triple7) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The mouse chases the mouse.
True
6
proof
[(((((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7)) -> rule3))]
("mouse" "chases" "mouse" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The mouse does not chase the mouse.
False
6
inv-proof
[(((((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7)) -> rule3))]
("mouse" "chases" "mouse" "-")
((((((((((triple7) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The tiger is not red.
Unknown
inv-rconc
[@2: The tiger is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("tiger" "is" "red" "-")
The cat is cold.
Unknown
rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "is" "cold" "+")
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("mouse" "is" "cold" "+")
The tiger does not chase the mouse.
Unknown
inv-rconc
[@3: The tiger chases the mouse.[CWA. Example of deepest failure = (rule3 <- rule4 <- rule1 <- FAIL)]]
("tiger" "chases" "mouse" "-")
The cat is red.
Unknown
rconc
[@2: The cat is red.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("cat" "is" "red" "+")
The mouse does not visit the cat.
Unknown
inv-random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "-")
The cow sees the cow.
Unknown
random
[@0: The cow sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "sees" "cow" "+")
The cat does not see the cat.
Unknown
inv-random
[@0: The cat sees the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "sees" "cat" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
The tiger is not round.
Unknown
inv-random
[@0: The tiger is round.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "round" "-")
The tiger chases the cat.
Unknown
random
[@0: The tiger chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "cat" "+")
@0: The cat visits the mouse.[(triple1)] The cow is young.[(triple2)] The cow sees the tiger.[(triple3)] The mouse chases the cat.[(triple4)] The mouse does not visit the cow.[(triple8)] The mouse is young.[(triple5)] The mouse sees the cat.[(triple6)] The mouse sees the cow.[(triple7)] The tiger visits the cow.[(triple9)] The tiger visits the mouse.[(triple10)] @1: The cow is cold.[(((triple7) -> rule5))] @2: The cow is red.[(((((triple7) -> rule5)) -> rule4))] @3: The cow chases the mouse.[(((((((triple7) -> rule5)) -> rule4)) -> rule3))] @4: The mouse is red.[(((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7))] @5: The mouse chases the mouse.[(((((((((((triple7) -> rule5)) -> rule4)) -> rule3)) -> rule7)) -> rule3))]
The cat visits the mouse.
("cat" "visits" "mouse" "+")
triple1
The cow is young.
("cow" "is" "young" "+")
triple2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
triple3
The mouse chases the cat.
("mouse" "chases" "cat" "+")
triple4
The mouse does not visit the cow.
("mouse" "visits" "cow" "-")
triple8
The mouse is young.
("mouse" "is" "young" "+")
triple5
The mouse sees the cat.
("mouse" "sees" "cat" "+")
triple6
The mouse sees the cow.
("mouse" "sees" "cow" "+")
triple7
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple9
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple10
The cow is cold.
("cow" "is" "cold" "+")
((triple7) -> (rule5 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow is red.
("cow" "is" "red" "+")
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
The cow is red.
("cow" "is" "red" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
((((((triple7) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int1
The cow is red.
("cow" "is" "red" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The mouse is red.
("mouse" "is" "red" "+")
((((((((triple7) -> (rule5 % int4))) -> (rule4 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The mouse is red.
("mouse" "is" "red" "+")
int1
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int2
The cow is red.
("cow" "is" "red" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
((((((((((triple7) -> (rule5 % int5))) -> (rule4 % int4))) -> (rule3 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
The mouse chases the mouse.
("mouse" "chases" "mouse" "+")
int1
The mouse is red.
("mouse" "is" "red" "+")
int2
The cow chases the mouse.
("cow" "chases" "mouse" "+")
int3
The cow is red.
("cow" "is" "red" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5