The bear is kind. The cow likes the squirrel. The squirrel likes the tiger. The squirrel visits the bear. The squirrel does not visit the cow. The tiger is not nice. The tiger visits the cow. If something is cold and it likes the bear then it visits the bear. If something chases the bear and the bear is kind then it likes the bear. If the tiger visits the cow then the tiger chases the squirrel. If something visits the bear then the bear likes the squirrel. If something likes the bear and it is not nice then the bear visits the squirrel. If something likes the bear then it visits the tiger. If something visits the cow then it chases the bear. If the bear likes the squirrel and the bear likes the tiger then the squirrel likes the cow.
The bear is kind.
("bear" "is" "kind" "+")
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
The squirrel does not visit the cow.
("squirrel" "visits" "cow" "-")
The tiger is not nice.
("tiger" "is" "nice" "-")
The tiger visits the cow.
("tiger" "visits" "cow" "+")
If something is cold and it likes the bear then it visits the bear.
((("something" "is" "cold" "+") ("something" "likes" "bear" "+")) -> ("something" "visits" "bear" "+"))
If something chases the bear and the bear is kind then it likes the bear.
((("something" "chases" "bear" "+") ("bear" "is" "kind" "+")) -> ("something" "likes" "bear" "+"))
If the tiger visits the cow then the tiger chases the squirrel.
((("tiger" "visits" "cow" "+")) -> ("tiger" "chases" "squirrel" "+"))
If something visits the bear then the bear likes the squirrel.
((("something" "visits" "bear" "+")) -> ("bear" "likes" "squirrel" "+"))
If something likes the bear and it is not nice then the bear visits the squirrel.
((("something" "likes" "bear" "+") ("something" "is" "nice" "~")) -> ("bear" "visits" "squirrel" "+"))
If something likes the bear then it visits the tiger.
((("something" "likes" "bear" "+")) -> ("something" "visits" "tiger" "+"))
If something visits the cow then it chases the bear.
((("something" "visits" "cow" "+")) -> ("something" "chases" "bear" "+"))
If the bear likes the squirrel and the bear likes the tiger then the squirrel likes the cow.
((("bear" "likes" "squirrel" "+") ("bear" "likes" "tiger" "+")) -> ("squirrel" "likes" "cow" "+"))
The cow likes the squirrel.
True
1
proof
[(triple2)]
("cow" "likes" "squirrel" "+")
triple2
The tiger does not visit the cow.
False
1
inv-proof
[(triple7)]
("tiger" "visits" "cow" "-")
triple7
The tiger chases the bear.
True
2
proof
[(((triple7) -> rule7))]
("tiger" "chases" "bear" "+")
((triple7) -> (rule7 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger does not chase the squirrel.
False
2
inv-proof
[(((triple7) -> rule3))]
("tiger" "chases" "squirrel" "-")
((triple7) -> (rule3 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger likes the bear.
True
4
proof
[(((((triple7) -> rule7) triple1) -> rule2))]
("tiger" "likes" "bear" "+")
((((triple7) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The tiger does not like the bear.
False
4
inv-proof
[(((((triple7) -> rule7) triple1) -> rule2))]
("tiger" "likes" "bear" "-")
((((triple7) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The tiger visits the tiger.
True
5
proof
[(((((((triple7) -> rule7) triple1) -> rule2)) -> rule6))]
("tiger" "visits" "tiger" "+")
((((((triple7) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int3
The tiger does not visit the tiger.
False
5
inv-proof
[(((((((triple7) -> rule7) triple1) -> rule2)) -> rule6))]
("tiger" "visits" "tiger" "-")
((((((triple7) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int3
The bear does not chase the bear.
Unknown
inv-rconc
[@1: The bear chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("bear" "chases" "bear" "-")
The squirrel chases the bear.
Unknown
rconc
[@1: The squirrel chases the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("squirrel" "chases" "bear" "+")
The bear does not visit the bear.
Unknown
inv-rconc
[@1: The bear visits the bear.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "visits" "bear" "-")
The cow likes the bear.
Unknown
rconc
[@2: The cow likes the bear.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("cow" "likes" "bear" "+")
The bear does not chase the tiger.
Unknown
inv-random
[@0: The bear chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "tiger" "-")
The cow is nice.
Unknown
random
[@0: The cow is nice.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "nice" "+")
The cow is not kind.
Unknown
inv-random
[@0: The cow is kind.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "kind" "-")
The squirrel chases the tiger.
Unknown
random
[@0: The squirrel chases the tiger.[CWA. Example of deepest failure = (FAIL)]]
("squirrel" "chases" "tiger" "+")
@0: The bear is kind.[(triple1)] The cow likes the squirrel.[(triple2)] The squirrel does not visit the cow.[(triple5)] The squirrel likes the tiger.[(triple3)] The squirrel visits the bear.[(triple4)] The tiger is not nice.[(triple6)] The tiger visits the cow.[(triple7)] @1: The bear likes the squirrel.[(((triple4) -> rule4))] The tiger chases the bear.[(((triple7) -> rule7))] The tiger chases the squirrel.[(((triple7) -> rule3))] @2: The tiger likes the bear.[(((((triple7) -> rule7) triple1) -> rule2))] @3: The bear visits the squirrel.[(((((((triple7) -> rule7) triple1) -> rule2) triple6) -> rule5))] The tiger visits the tiger.[(((((((triple7) -> rule7) triple1) -> rule2)) -> rule6))]
The bear is kind.
("bear" "is" "kind" "+")
triple1
The cow likes the squirrel.
("cow" "likes" "squirrel" "+")
triple2
The squirrel does not visit the cow.
("squirrel" "visits" "cow" "-")
triple5
The squirrel likes the tiger.
("squirrel" "likes" "tiger" "+")
triple3
The squirrel visits the bear.
("squirrel" "visits" "bear" "+")
triple4
The tiger is not nice.
("tiger" "is" "nice" "-")
triple6
The tiger visits the cow.
("tiger" "visits" "cow" "+")
triple7
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
((triple4) -> (rule4 % int1))
The bear likes the squirrel.
("bear" "likes" "squirrel" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
((triple7) -> (rule7 % int1))
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int1
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
((triple7) -> (rule3 % int1))
The tiger chases the squirrel.
("tiger" "chases" "squirrel" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
((((triple7) -> (rule7 % int2)) triple1) -> (rule2 % int1))
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int1
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int2
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
((((((triple7) -> (rule7 % int3)) triple1) -> (rule2 % int2)) triple6) -> (rule5 % int1))
The bear visits the squirrel.
("bear" "visits" "squirrel" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int3
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
((((((triple7) -> (rule7 % int3)) triple1) -> (rule2 % int2))) -> (rule6 % int1))
The tiger visits the tiger.
("tiger" "visits" "tiger" "+")
int1
The tiger likes the bear.
("tiger" "likes" "bear" "+")
int2
The tiger chases the bear.
("tiger" "chases" "bear" "+")
int3