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