The bear is rough. The bear does not visit the mouse. The cat likes the tiger. The mouse is not green. The mouse is rough. The mouse likes the bear. The mouse likes the cat. The mouse does not see the cat. The mouse visits the bear. The tiger is big. The tiger is green. The tiger is rough. The tiger is round. The tiger likes the mouse. The tiger visits the cat. The tiger visits the mouse. If something sees the bear and it visits the mouse then the mouse does not like the cat. If something visits the cat then the cat is round. If the tiger visits the cat and the cat sees the bear then the cat is green. If something sees the mouse and the mouse likes the cat then the mouse is kind. If something is round then it sees the cat. If the cat sees the tiger then the tiger sees the cat. If something sees the cat then it sees the tiger. If something visits the mouse and it is not green then the mouse sees the cat.
The bear is rough.
("bear" "is" "rough" "+")
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
The cat likes the tiger.
("cat" "likes" "tiger" "+")
The mouse is not green.
("mouse" "is" "green" "-")
The mouse is rough.
("mouse" "is" "rough" "+")
The mouse likes the bear.
("mouse" "likes" "bear" "+")
The mouse likes the cat.
("mouse" "likes" "cat" "+")
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
The mouse visits the bear.
("mouse" "visits" "bear" "+")
The tiger is big.
("tiger" "is" "big" "+")
The tiger is green.
("tiger" "is" "green" "+")
The tiger is rough.
("tiger" "is" "rough" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
The tiger visits the cat.
("tiger" "visits" "cat" "+")
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
If something sees the bear and it visits the mouse then the mouse does not like the cat.
((("something" "sees" "bear" "+") ("something" "visits" "mouse" "+")) -> ("mouse" "likes" "cat" "-"))
If something visits the cat then the cat is round.
((("something" "visits" "cat" "+")) -> ("cat" "is" "round" "+"))
If the tiger visits the cat and the cat sees the bear then the cat is green.
((("tiger" "visits" "cat" "+") ("cat" "sees" "bear" "+")) -> ("cat" "is" "green" "+"))
If something sees the mouse and the mouse likes the cat then the mouse is kind.
((("something" "sees" "mouse" "+") ("mouse" "likes" "cat" "+")) -> ("mouse" "is" "kind" "+"))
If something is round then it sees the cat.
((("something" "is" "round" "+")) -> ("something" "sees" "cat" "+"))
If the cat sees the tiger then the tiger sees the cat.
((("cat" "sees" "tiger" "+")) -> ("tiger" "sees" "cat" "+"))
If something sees the cat then it sees the tiger.
((("something" "sees" "cat" "+")) -> ("something" "sees" "tiger" "+"))
If something visits the mouse and it is not green then the mouse sees the cat.
((("something" "visits" "mouse" "+") ("something" "is" "green" "~")) -> ("mouse" "sees" "cat" "+"))
The tiger is rough.
True
1
proof
[(triple12)]
("tiger" "is" "rough" "+")
triple12
The bear is not rough.
False
1
inv-proof
[(triple1)]
("bear" "is" "rough" "-")
triple1
The tiger sees the cat.
True
2
proof
[(((triple13) -> rule5) OR ((((((((triple15) -> rule2)) -> rule5)) -> rule7)) -> rule6))]
("tiger" "sees" "cat" "+")
((triple13) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
((((((((triple15) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The cat is not round.
False
2
inv-proof
[(((triple15) -> rule2))]
("cat" "is" "round" "-")
((triple15) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple13) -> rule5)) -> rule7) OR ((((((((((triple15) -> rule2)) -> rule5)) -> rule7)) -> rule6)) -> rule7))]
("tiger" "sees" "tiger" "+")
((((triple13) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((((((triple15) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple13) -> rule5)) -> rule7) OR ((((((((((triple15) -> rule2)) -> rule5)) -> rule7)) -> rule6)) -> rule7))]
("tiger" "sees" "tiger" "-")
((((triple13) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((((((triple15) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The cat sees the tiger.
True
4
proof
[(((((((triple15) -> rule2)) -> rule5)) -> rule7))]
("cat" "sees" "tiger" "+")
((((((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The cat does not see the tiger.
False
4
inv-proof
[(((((((triple15) -> rule2)) -> rule5)) -> rule7))]
("cat" "sees" "tiger" "-")
((((((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3
The bear does not see the tiger.
Unknown
inv-rconc
[@2: The bear sees the tiger.[CWA. Example of deepest failure = (rule7 <- rule5 <- FAIL)]]
("bear" "sees" "tiger" "-")
The bear sees the cat.
Unknown
rconc
[@1: The bear sees the cat.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "sees" "cat" "+")
The mouse does not see the tiger.
Unknown
inv-rconc
[@1: The mouse sees the tiger.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("mouse" "sees" "tiger" "-")
The mouse is kind.
Unknown
rconc
[@1: The mouse is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("mouse" "is" "kind" "+")
The bear is not round.
Unknown
inv-random
[@0: The bear is round.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "round" "-")
The mouse visits the cat.
Unknown
random
[@0: The mouse visits the cat.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "visits" "cat" "+")
The bear does not see the bear.
Unknown
inv-random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "-")
The bear likes the tiger.
Unknown
random
[@0: The bear likes the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "tiger" "+")
@0: The bear does not visit the mouse.[(triple2)] The bear is rough.[(triple1)] The cat likes the tiger.[(triple3)] The mouse does not see the cat.[(triple8)] The mouse is not green.[(triple4)] The mouse is rough.[(triple5)] The mouse likes the bear.[(triple6)] The mouse likes the cat.[(triple7)] The mouse visits the bear.[(triple9)] The tiger is big.[(triple10)] The tiger is green.[(triple11)] The tiger is rough.[(triple12)] The tiger is round.[(triple13)] The tiger likes the mouse.[(triple14)] The tiger visits the cat.[(triple15)] The tiger visits the mouse.[(triple16)] @1: The cat is round.[(((triple15) -> rule2))] The tiger sees the cat.[(((triple13) -> rule5) OR ((((((((triple15) -> rule2)) -> rule5)) -> rule7)) -> rule6))] @2: The cat sees the cat.[(((((triple15) -> rule2)) -> rule5))] The tiger sees the tiger.[(((((triple13) -> rule5)) -> rule7) OR ((((((((((triple15) -> rule2)) -> rule5)) -> rule7)) -> rule6)) -> rule7))] @3: The cat sees the tiger.[(((((((triple15) -> rule2)) -> rule5)) -> rule7))]
The bear does not visit the mouse.
("bear" "visits" "mouse" "-")
triple2
The bear is rough.
("bear" "is" "rough" "+")
triple1
The cat likes the tiger.
("cat" "likes" "tiger" "+")
triple3
The mouse does not see the cat.
("mouse" "sees" "cat" "-")
triple8
The mouse is not green.
("mouse" "is" "green" "-")
triple4
The mouse is rough.
("mouse" "is" "rough" "+")
triple5
The mouse likes the bear.
("mouse" "likes" "bear" "+")
triple6
The mouse likes the cat.
("mouse" "likes" "cat" "+")
triple7
The mouse visits the bear.
("mouse" "visits" "bear" "+")
triple9
The tiger is big.
("tiger" "is" "big" "+")
triple10
The tiger is green.
("tiger" "is" "green" "+")
triple11
The tiger is rough.
("tiger" "is" "rough" "+")
triple12
The tiger is round.
("tiger" "is" "round" "+")
triple13
The tiger likes the mouse.
("tiger" "likes" "mouse" "+")
triple14
The tiger visits the cat.
("tiger" "visits" "cat" "+")
triple15
The tiger visits the mouse.
("tiger" "visits" "mouse" "+")
triple16
The cat is round.
("cat" "is" "round" "+")
((triple15) -> (rule2 % int1))
The cat is round.
("cat" "is" "round" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
((triple13) -> (rule5 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
((((((((triple15) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule7 % int2))) -> (rule6 % int1))
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int1
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int2
The cat sees the cat.
("cat" "sees" "cat" "+")
int3
The cat is round.
("cat" "is" "round" "+")
int4
The cat sees the cat.
("cat" "sees" "cat" "+")
((((triple15) -> (rule2 % int2))) -> (rule5 % int1))
The cat sees the cat.
("cat" "sees" "cat" "+")
int1
The cat is round.
("cat" "is" "round" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple13) -> (rule5 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
((((((((((triple15) -> (rule2 % int5))) -> (rule5 % int4))) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule7 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger sees the cat.
("tiger" "sees" "cat" "+")
int2
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int3
The cat sees the cat.
("cat" "sees" "cat" "+")
int4
The cat is round.
("cat" "is" "round" "+")
int5
The cat sees the tiger.
("cat" "sees" "tiger" "+")
((((((triple15) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
The cat sees the tiger.
("cat" "sees" "tiger" "+")
int1
The cat sees the cat.
("cat" "sees" "cat" "+")
int2
The cat is round.
("cat" "is" "round" "+")
int3