The bear sees the mouse. The cow eats the dog. The cow is nice. The cow is young. The cow likes the bear. The cow sees the mouse. The dog is big. The dog is young. The dog likes the cow. The dog likes the mouse. The mouse eats the bear. If someone is cold then they see the dog. If someone is young then they see the bear. If someone likes the bear then they are cold. If someone sees the cow then the cow eats the mouse. If someone is young and they see the mouse then they are big. If someone is cold and they see the dog then the dog likes the bear. If someone likes the dog then the dog sees the bear. If the bear is cold then the bear sees the dog.
The bear sees the mouse.
("bear" "sees" "mouse" "+")
The cow eats the dog.
("cow" "eats" "dog" "+")
The cow is nice.
("cow" "is" "nice" "+")
The cow is young.
("cow" "is" "young" "+")
The cow likes the bear.
("cow" "likes" "bear" "+")
The cow sees the mouse.
("cow" "sees" "mouse" "+")
The dog is big.
("dog" "is" "big" "+")
The dog is young.
("dog" "is" "young" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The dog likes the mouse.
("dog" "likes" "mouse" "+")
The mouse eats the bear.
("mouse" "eats" "bear" "+")
If someone is cold then they see the dog.
((("someone" "is" "cold" "+")) -> ("someone" "sees" "dog" "+"))
If someone is young then they see the bear.
((("someone" "is" "young" "+")) -> ("someone" "sees" "bear" "+"))
If someone likes the bear then they are cold.
((("someone" "likes" "bear" "+")) -> ("someone" "is" "cold" "+"))
If someone sees the cow then the cow eats the mouse.
((("someone" "sees" "cow" "+")) -> ("cow" "eats" "mouse" "+"))
If someone is young and they see the mouse then they are big.
((("someone" "is" "young" "+") ("someone" "sees" "mouse" "+")) -> ("someone" "is" "big" "+"))
If someone is cold and they see the dog then the dog likes the bear.
((("someone" "is" "cold" "+") ("someone" "sees" "dog" "+")) -> ("dog" "likes" "bear" "+"))
If someone likes the dog then the dog sees the bear.
((("someone" "likes" "dog" "+")) -> ("dog" "sees" "bear" "+"))
If the bear is cold then the bear sees the dog.
((("bear" "is" "cold" "+")) -> ("bear" "sees" "dog" "+"))
The dog is big.
True
1
proof
[(triple7)]
("dog" "is" "big" "+")
triple7
The dog is not young.
False
1
inv-proof
[(triple8)]
("dog" "is" "young" "-")
triple8
The cow is big.
True
3
proof
[(((triple4 triple6) -> rule5))]
("cow" "is" "big" "+")
((triple4 triple6) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is not cold.
False
2
inv-proof
[(((triple5) -> rule3))]
("cow" "is" "cold" "-")
((triple5) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the dog.
True
3
proof
[(((((triple5) -> rule3)) -> rule1))]
("cow" "sees" "dog" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The cow does not see the dog.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule1))]
("cow" "sees" "dog" "-")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The dog likes the bear.
True
6
proof
[(((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6))]
("dog" "likes" "bear" "+")
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The dog does not like the bear.
False
6
inv-proof
[(((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6))]
("dog" "likes" "bear" "-")
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The dog is cold.
True
7
proof
[(((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("dog" "is" "cold" "+")
((((((triple5) -> (rule3 % int4)) ((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The dog is not cold.
False
7
inv-proof
[(((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3))]
("dog" "is" "cold" "-")
((((((triple5) -> (rule3 % int4)) ((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The dog sees the dog.
True
8
proof
[(((((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
("dog" "sees" "dog" "+")
((((((((triple5) -> (rule3 % int5)) ((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The dog does not see the dog.
False
8
inv-proof
[(((((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
("dog" "sees" "dog" "-")
((((((((triple5) -> (rule3 % int5)) ((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5
The mouse does not see the bear.
Unknown
inv-rconc
[@1: The mouse sees the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("mouse" "sees" "bear" "-")
The mouse is cold.
Unknown
rconc
[@1: The mouse is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("mouse" "is" "cold" "+")
The bear is not big.
Unknown
inv-rconc
[@1: The bear is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "is" "big" "-")
The mouse sees the dog.
Unknown
rconc
[@2: The mouse sees the dog.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("mouse" "sees" "dog" "+")
The mouse is not big.
Unknown
inv-rconc
[@1: The mouse is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("mouse" "is" "big" "-")
The bear is cold.
Unknown
rconc
[@1: The bear is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("bear" "is" "cold" "+")
The dog does not eat the cow.
Unknown
inv-random
[@0: The dog eats the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "eats" "cow" "-")
The mouse is young.
Unknown
random
[@0: The mouse is young.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "is" "young" "+")
The dog does not like the dog.
Unknown
inv-random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "-")
The bear eats the bear.
Unknown
random
[@0: The bear eats the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "eats" "bear" "+")
The cow does not like the mouse.
Unknown
inv-random
[@0: The cow likes the mouse.[CWA. Example of deepest failure = (FAIL)]]
("cow" "likes" "mouse" "-")
The mouse sees the cow.
Unknown
random
[@0: The mouse sees the cow.[CWA. Example of deepest failure = (FAIL)]]
("mouse" "sees" "cow" "+")
@0: The bear sees the mouse.[(triple1)] The cow eats the dog.[(triple2)] The cow is nice.[(triple3)] The cow is young.[(triple4)] The cow likes the bear.[(triple5)] The cow sees the mouse.[(triple6)] The dog is big.[(triple7)] The dog is young.[(triple8)] The dog likes the cow.[(triple9)] The dog likes the mouse.[(triple10)] The mouse eats the bear.[(triple11)] @1: The cow is big.[(((triple4 triple6) -> rule5))] The cow is cold.[(((triple5) -> rule3))] The cow sees the bear.[(((triple4) -> rule2))] The dog sees the bear.[(((triple8) -> rule2))] @2: The cow sees the dog.[(((((triple5) -> rule3)) -> rule1))] @3: The dog likes the bear.[(((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6))] @4: The dog is cold.[(((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3))] @5: The dog sees the dog.[(((((((((triple5) -> rule3) ((((triple5) -> rule3)) -> rule1)) -> rule6)) -> rule3)) -> rule1))]
The bear sees the mouse.
("bear" "sees" "mouse" "+")
triple1
The cow eats the dog.
("cow" "eats" "dog" "+")
triple2
The cow is nice.
("cow" "is" "nice" "+")
triple3
The cow is young.
("cow" "is" "young" "+")
triple4
The cow likes the bear.
("cow" "likes" "bear" "+")
triple5
The cow sees the mouse.
("cow" "sees" "mouse" "+")
triple6
The dog is big.
("dog" "is" "big" "+")
triple7
The dog is young.
("dog" "is" "young" "+")
triple8
The dog likes the cow.
("dog" "likes" "cow" "+")
triple9
The dog likes the mouse.
("dog" "likes" "mouse" "+")
triple10
The mouse eats the bear.
("mouse" "eats" "bear" "+")
triple11
The cow is big.
("cow" "is" "big" "+")
((triple4 triple6) -> (rule5 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
((triple5) -> (rule3 % int1))
The cow is cold.
("cow" "is" "cold" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
((triple4) -> (rule2 % int1))
The cow sees the bear.
("cow" "sees" "bear" "+")
int1
The dog sees the bear.
("dog" "sees" "bear" "+")
((triple8) -> (rule2 % int1))
The dog sees the bear.
("dog" "sees" "bear" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The cow is cold.
("cow" "is" "cold" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
((((triple5) -> (rule3 % int3)) ((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule6 % int1))
The dog likes the bear.
("dog" "likes" "bear" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is cold.
("cow" "is" "cold" "+")
int3
The dog is cold.
("dog" "is" "cold" "+")
((((((triple5) -> (rule3 % int4)) ((((triple5) -> (rule3 % int4))) -> (rule1 % int3))) -> (rule6 % int2))) -> (rule3 % int1))
The dog is cold.
("dog" "is" "cold" "+")
int1
The dog likes the bear.
("dog" "likes" "bear" "+")
int2
The cow sees the dog.
("cow" "sees" "dog" "+")
int3
The cow is cold.
("cow" "is" "cold" "+")
int4
The dog sees the dog.
("dog" "sees" "dog" "+")
((((((((triple5) -> (rule3 % int5)) ((((triple5) -> (rule3 % int5))) -> (rule1 % int4))) -> (rule6 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The dog is cold.
("dog" "is" "cold" "+")
int2
The dog likes the bear.
("dog" "likes" "bear" "+")
int3
The cow sees the dog.
("cow" "sees" "dog" "+")
int4
The cow is cold.
("cow" "is" "cold" "+")
int5