The cow eats the rabbit. The cow eats the squirrel. The cow eats the tiger. The cow is cold. The cow is rough. The cow sees the rabbit. The cow visits the rabbit. The cow visits the squirrel. The rabbit eats the squirrel. The rabbit is kind. The squirrel eats the cow. The squirrel visits the cow. The squirrel visits the tiger. The tiger is kind. The tiger is rough. The tiger visits the squirrel. If someone eats the squirrel then they visit the rabbit. If someone sees the cow then they are big. If someone eats the squirrel then they eat the rabbit. If someone is green then they are rough. If someone is kind then they eat the squirrel. If someone is green then they visit the tiger. If someone eats the rabbit then they are cold. If someone sees the cow then the cow is kind.
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
The cow eats the tiger.
("cow" "eats" "tiger" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow is rough.
("cow" "is" "rough" "+")
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
The rabbit is kind.
("rabbit" "is" "kind" "+")
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
The tiger is kind.
("tiger" "is" "kind" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
If someone eats the squirrel then they visit the rabbit.
((("someone" "eats" "squirrel" "+")) -> ("someone" "visits" "rabbit" "+"))
If someone sees the cow then they are big.
((("someone" "sees" "cow" "+")) -> ("someone" "is" "big" "+"))
If someone eats the squirrel then they eat the rabbit.
((("someone" "eats" "squirrel" "+")) -> ("someone" "eats" "rabbit" "+"))
If someone is green then they are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If someone is kind then they eat the squirrel.
((("someone" "is" "kind" "+")) -> ("someone" "eats" "squirrel" "+"))
If someone is green then they visit the tiger.
((("someone" "is" "green" "+")) -> ("someone" "visits" "tiger" "+"))
If someone eats the rabbit then they are cold.
((("someone" "eats" "rabbit" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cow then the cow is kind.
((("someone" "sees" "cow" "+")) -> ("cow" "is" "kind" "+"))
The cow visits the squirrel.
True
1
proof
[(triple8)]
("cow" "visits" "squirrel" "+")
triple8
The squirrel does not visit the tiger.
False
1
inv-proof
[(triple13)]
("squirrel" "visits" "tiger" "-")
triple13
The rabbit eats the rabbit.
True
2
proof
[(((triple9) -> rule3) OR ((((triple10) -> rule5)) -> rule3))]
("rabbit" "eats" "rabbit" "+")
((triple9) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit does not eat the rabbit.
False
2
inv-proof
[(((triple9) -> rule3) OR ((((triple10) -> rule5)) -> rule3))]
("rabbit" "eats" "rabbit" "-")
((triple9) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The tiger eats the rabbit.
True
3
proof
[(((((triple14) -> rule5)) -> rule3))]
("tiger" "eats" "rabbit" "+")
((((triple14) -> (rule5 % int2))) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The rabbit is not cold.
False
3
inv-proof
[(((((triple9) -> rule3)) -> rule7) OR ((((((triple10) -> rule5)) -> rule3)) -> rule7))]
("rabbit" "is" "cold" "-")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The tiger is cold.
True
4
proof
[(((((((triple14) -> rule5)) -> rule3)) -> rule7))]
("tiger" "is" "cold" "+")
((((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger is not cold.
False
4
inv-proof
[(((((((triple14) -> rule5)) -> rule3)) -> rule7))]
("tiger" "is" "cold" "-")
((((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3
The tiger is not big.
Unknown
inv-rconc
[@1: The tiger is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "big" "-")
The squirrel is cold.
Unknown
rconc
[@3: The squirrel is cold.[CWA. Example of deepest failure = (rule7 <- rule3 <- rule5 <- FAIL)]]
("squirrel" "is" "cold" "+")
The squirrel is not rough.
Unknown
inv-rconc
[@1: The squirrel is rough.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("squirrel" "is" "rough" "-")
The squirrel is big.
Unknown
rconc
[@1: The squirrel is big.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("squirrel" "is" "big" "+")
The squirrel does not visit the squirrel.
Unknown
inv-random
[@0: The squirrel visits the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "visits" "squirrel" "-")
The rabbit sees the cow.
Unknown
random
[@0: The rabbit sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "sees" "cow" "+")
The rabbit does not visit the cow.
Unknown
inv-random
[@0: The rabbit visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "cow" "-")
The tiger sees the squirrel.
Unknown
random
[@0: The tiger sees the squirrel.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "sees" "squirrel" "+")
@0: The cow eats the rabbit.[(triple1 OR ((triple2) -> rule3))] The cow eats the squirrel.[(triple2)] The cow eats the tiger.[(triple3)] The cow is cold.[(triple4 OR ((triple1) -> rule7) OR ((((triple2) -> rule3)) -> rule7))] The cow is rough.[(triple5)] The cow sees the rabbit.[(triple6)] The cow visits the rabbit.[(triple7 OR ((triple2) -> rule1))] The cow visits the squirrel.[(triple8)] The rabbit eats the squirrel.[(triple9 OR ((triple10) -> rule5))] The rabbit is kind.[(triple10)] The squirrel eats the cow.[(triple11)] The squirrel visits the cow.[(triple12)] The squirrel visits the tiger.[(triple13)] The tiger is kind.[(triple14)] The tiger is rough.[(triple15)] The tiger visits the squirrel.[(triple16)] @1: The rabbit eats the rabbit.[(((triple9) -> rule3) OR ((((triple10) -> rule5)) -> rule3))] The rabbit visits the rabbit.[(((triple9) -> rule1) OR ((((triple10) -> rule5)) -> rule1))] The tiger eats the squirrel.[(((triple14) -> rule5))] @2: The rabbit is cold.[(((((triple9) -> rule3)) -> rule7) OR ((((((triple10) -> rule5)) -> rule3)) -> rule7))] The tiger eats the rabbit.[(((((triple14) -> rule5)) -> rule3))] The tiger visits the rabbit.[(((((triple14) -> rule5)) -> rule1))] @3: The tiger is cold.[(((((((triple14) -> rule5)) -> rule3)) -> rule7))]
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
triple1
((triple2) -> (rule3 % int1))
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int1
The cow eats the squirrel.
("cow" "eats" "squirrel" "+")
triple2
The cow eats the tiger.
("cow" "eats" "tiger" "+")
triple3
The cow is cold.
("cow" "is" "cold" "+")
triple4
((triple1) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
((((triple2) -> (rule3 % int2))) -> (rule7 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow eats the rabbit.
("cow" "eats" "rabbit" "+")
int2
The cow is rough.
("cow" "is" "rough" "+")
triple5
The cow sees the rabbit.
("cow" "sees" "rabbit" "+")
triple6
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
triple7
((triple2) -> (rule1 % int1))
The cow visits the rabbit.
("cow" "visits" "rabbit" "+")
int1
The cow visits the squirrel.
("cow" "visits" "squirrel" "+")
triple8
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
triple9
((triple10) -> (rule5 % int1))
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int1
The rabbit is kind.
("rabbit" "is" "kind" "+")
triple10
The squirrel eats the cow.
("squirrel" "eats" "cow" "+")
triple11
The squirrel visits the cow.
("squirrel" "visits" "cow" "+")
triple12
The squirrel visits the tiger.
("squirrel" "visits" "tiger" "+")
triple13
The tiger is kind.
("tiger" "is" "kind" "+")
triple14
The tiger is rough.
("tiger" "is" "rough" "+")
triple15
The tiger visits the squirrel.
("tiger" "visits" "squirrel" "+")
triple16
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
((triple9) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
((triple9) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
The rabbit visits the rabbit.
("rabbit" "visits" "rabbit" "+")
int1
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
((triple14) -> (rule5 % int1))
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int1
The rabbit is cold.
("rabbit" "is" "cold" "+")
((((triple9) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The rabbit is cold.
("rabbit" "is" "cold" "+")
int1
The rabbit eats the rabbit.
("rabbit" "eats" "rabbit" "+")
int2
The rabbit eats the squirrel.
("rabbit" "eats" "squirrel" "+")
int3
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
((((triple14) -> (rule5 % int2))) -> (rule3 % int1))
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
((((triple14) -> (rule5 % int2))) -> (rule1 % int1))
The tiger visits the rabbit.
("tiger" "visits" "rabbit" "+")
int1
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int2
The tiger is cold.
("tiger" "is" "cold" "+")
((((((triple14) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule7 % int1))
The tiger is cold.
("tiger" "is" "cold" "+")
int1
The tiger eats the rabbit.
("tiger" "eats" "rabbit" "+")
int2
The tiger eats the squirrel.
("tiger" "eats" "squirrel" "+")
int3