The bear chases the tiger. The bear visits the tiger. The cow chases the bear. The cow does not chase the tiger. The cow sees the dog. The cow visits the dog. The dog is cold. The dog sees the bear. The dog sees the tiger. The tiger is round. The tiger sees the cow. The tiger visits the dog. If something chases the cow then it is cold. If something is rough then it sees the tiger. If something sees the bear and the bear sees the tiger then the tiger sees the dog. If something visits the dog then it is rough. If something visits the bear then it is rough. If something chases the bear and it is not round then the bear chases the dog. If something chases the tiger and the tiger is rough then it visits the bear.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow chases the bear.
("cow" "chases" "bear" "+")
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
The cow sees the dog.
("cow" "sees" "dog" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog is cold.
("dog" "is" "cold" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the tiger.
("dog" "sees" "tiger" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the cow.
("tiger" "sees" "cow" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something chases the cow then it is cold.
((("something" "chases" "cow" "+")) -> ("something" "is" "cold" "+"))
If something is rough then it sees the tiger.
((("something" "is" "rough" "+")) -> ("something" "sees" "tiger" "+"))
If something sees the bear and the bear sees the tiger then the tiger sees the dog.
((("something" "sees" "bear" "+") ("bear" "sees" "tiger" "+")) -> ("tiger" "sees" "dog" "+"))
If something visits the dog then it is rough.
((("something" "visits" "dog" "+")) -> ("something" "is" "rough" "+"))
If something visits the bear then it is rough.
((("something" "visits" "bear" "+")) -> ("something" "is" "rough" "+"))
If something chases the bear and it is not round then the bear chases the dog.
((("something" "chases" "bear" "+") ("something" "is" "round" "~")) -> ("bear" "chases" "dog" "+"))
If something chases the tiger and the tiger is rough then it visits the bear.
((("something" "chases" "tiger" "+") ("tiger" "is" "rough" "+")) -> ("something" "visits" "bear" "+"))
The cow sees the dog.
True
1
proof
[(triple5)]
("cow" "sees" "dog" "+")
triple5
The cow does not chase the bear.
False
1
inv-proof
[(triple3)]
("cow" "chases" "bear" "-")
triple3
The tiger is rough.
True
2
proof
[(((triple12) -> rule4))]
("tiger" "is" "rough" "+")
((triple12) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The cow is not rough.
False
2
inv-proof
[(((triple6) -> rule4))]
("cow" "is" "rough" "-")
((triple6) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The tiger sees the tiger.
True
3
proof
[(((((triple12) -> rule4)) -> rule2))]
("tiger" "sees" "tiger" "+")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The tiger does not see the tiger.
False
3
inv-proof
[(((((triple12) -> rule4)) -> rule2))]
("tiger" "sees" "tiger" "-")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear is rough.
True
5
proof
[(((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5))]
("bear" "is" "rough" "+")
((((triple1 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The bear is not rough.
False
5
inv-proof
[(((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5))]
("bear" "is" "rough" "-")
((((triple1 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The bear sees the tiger.
True
6
proof
[(((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2))]
("bear" "sees" "tiger" "+")
((((((triple1 ((triple12) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The bear does not see the tiger.
False
6
inv-proof
[(((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2))]
("bear" "sees" "tiger" "-")
((((((triple1 ((triple12) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The tiger sees the dog.
True
8
proof
[(((triple8 ((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2)) -> rule3))]
("tiger" "sees" "dog" "+")
((triple8 ((((((triple1 ((triple12) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5
The tiger does not see the dog.
False
8
inv-proof
[(((triple8 ((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2)) -> rule3))]
("tiger" "sees" "dog" "-")
((triple8 ((((((triple1 ((triple12) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5
The dog is not rough.
Unknown
inv-rconc
[@2: The dog is rough.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("dog" "is" "rough" "-")
The cow visits the bear.
Unknown
rconc
[@1: The cow visits the bear.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("cow" "visits" "bear" "+")
The cow is not cold.
Unknown
inv-rconc
[@1: The cow is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cow" "is" "cold" "-")
The tiger is cold.
Unknown
rconc
[@1: The tiger is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("tiger" "is" "cold" "+")
The bear does not chase the dog.
Unknown
inv-rconc
[@1: The bear chases the dog.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "chases" "dog" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("bear" "is" "cold" "+")
The cow is not blue.
Unknown
inv-random
[@0: The cow is blue.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "blue" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The bear does not visit the cow.
Unknown
inv-random
[@0: The bear visits the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "cow" "-")
The cow chases the cow.
Unknown
random
[@0: The cow chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "cow" "+")
The dog does not visit the dog.
Unknown
inv-random
[@0: The dog visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "visits" "dog" "-")
The bear chases the cow.
Unknown
random
[@0: The bear chases the cow.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "cow" "+")
@0: The bear chases the tiger.[(triple1)] The bear visits the tiger.[(triple2)] The cow chases the bear.[(triple3)] The cow does not chase the tiger.[(triple4)] The cow sees the dog.[(triple5)] The cow visits the dog.[(triple6)] The dog is cold.[(triple7)] The dog sees the bear.[(triple8)] The dog sees the tiger.[(triple9)] The tiger is round.[(triple10)] The tiger sees the cow.[(triple11)] The tiger visits the dog.[(triple12)] @1: The cow is rough.[(((triple6) -> rule4))] The tiger is rough.[(((triple12) -> rule4))] @2: The bear visits the bear.[(((triple1 ((triple12) -> rule4)) -> rule7))] The cow sees the tiger.[(((((triple6) -> rule4)) -> rule2))] The tiger sees the tiger.[(((((triple12) -> rule4)) -> rule2))] @3: The bear is rough.[(((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5))] @4: The bear sees the tiger.[(((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2))] @5: The tiger sees the dog.[(((triple8 ((((((triple1 ((triple12) -> rule4)) -> rule7)) -> rule5)) -> rule2)) -> rule3))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple2
The cow chases the bear.
("cow" "chases" "bear" "+")
triple3
The cow does not chase the tiger.
("cow" "chases" "tiger" "-")
triple4
The cow sees the dog.
("cow" "sees" "dog" "+")
triple5
The cow visits the dog.
("cow" "visits" "dog" "+")
triple6
The dog is cold.
("dog" "is" "cold" "+")
triple7
The dog sees the bear.
("dog" "sees" "bear" "+")
triple8
The dog sees the tiger.
("dog" "sees" "tiger" "+")
triple9
The tiger is round.
("tiger" "is" "round" "+")
triple10
The tiger sees the cow.
("tiger" "sees" "cow" "+")
triple11
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple12
The cow is rough.
("cow" "is" "rough" "+")
((triple6) -> (rule4 % int1))
The cow is rough.
("cow" "is" "rough" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
((triple12) -> (rule4 % int1))
The tiger is rough.
("tiger" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple1 ((triple12) -> (rule4 % int2))) -> (rule7 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The cow sees the tiger.
("cow" "sees" "tiger" "+")
((((triple6) -> (rule4 % int2))) -> (rule2 % int1))
The cow sees the tiger.
("cow" "sees" "tiger" "+")
int1
The cow is rough.
("cow" "is" "rough" "+")
int2
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
((((triple12) -> (rule4 % int2))) -> (rule2 % int1))
The tiger sees the tiger.
("tiger" "sees" "tiger" "+")
int1
The tiger is rough.
("tiger" "is" "rough" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
((((triple1 ((triple12) -> (rule4 % int3))) -> (rule7 % int2))) -> (rule5 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger is rough.
("tiger" "is" "rough" "+")
int3
The bear sees the tiger.
("bear" "sees" "tiger" "+")
((((((triple1 ((triple12) -> (rule4 % int4))) -> (rule7 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3
The tiger is rough.
("tiger" "is" "rough" "+")
int4
The tiger sees the dog.
("tiger" "sees" "dog" "+")
((triple8 ((((((triple1 ((triple12) -> (rule4 % int5))) -> (rule7 % int4))) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
The tiger sees the dog.
("tiger" "sees" "dog" "+")
int1
The bear sees the tiger.
("bear" "sees" "tiger" "+")
int2
The bear is rough.
("bear" "is" "rough" "+")
int3
The bear visits the bear.
("bear" "visits" "bear" "+")
int4
The tiger is rough.
("tiger" "is" "rough" "+")
int5