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