The bear is cold. The bear is round. The bear is young. The bear likes the cat. The bear likes the dog. The bear sees the cat. The bear sees the dog. The cat chases the bear. The cat likes the bear. The dog does not chase the cat. The dog is kind. The dog is not young. The dog likes the bear. The dog likes the cat. The dog sees the bear. The dog sees the cat. Rough things are kind. All rough, young things are kind. If something likes the dog then it chases the bear. If something likes the cat then it sees the dog. If something is rough and it does not like the bear then it is cold. If something is round and it chases the bear then the bear is rough.
The bear is cold.
("bear" "is" "cold" "+")
The bear is round.
("bear" "is" "round" "+")
The bear is young.
("bear" "is" "young" "+")
The bear likes the cat.
("bear" "likes" "cat" "+")
The bear likes the dog.
("bear" "likes" "dog" "+")
The bear sees the cat.
("bear" "sees" "cat" "+")
The bear sees the dog.
("bear" "sees" "dog" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat likes the bear.
("cat" "likes" "bear" "+")
The dog does not chase the cat.
("dog" "chases" "cat" "-")
The dog is kind.
("dog" "is" "kind" "+")
The dog is not young.
("dog" "is" "young" "-")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the cat.
("dog" "likes" "cat" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the cat.
("dog" "sees" "cat" "+")
Rough things are kind.
((("something" "is" "rough" "+")) -> ("something" "is" "kind" "+"))
All rough, young things are kind.
((("something" "is" "rough" "+") ("something" "is" "young" "+")) -> ("something" "is" "kind" "+"))
If something likes the dog then it chases the bear.
((("something" "likes" "dog" "+")) -> ("something" "chases" "bear" "+"))
If something likes the cat then it sees the dog.
((("something" "likes" "cat" "+")) -> ("something" "sees" "dog" "+"))
If something is rough and it does not like the bear then it is cold.
((("something" "is" "rough" "+") ("something" "likes" "bear" "~")) -> ("something" "is" "cold" "+"))
If something is round and it chases the bear then the bear is rough.
((("something" "is" "round" "+") ("something" "chases" "bear" "+")) -> ("bear" "is" "rough" "+"))
The dog sees the bear.
True
1
proof
[(triple15)]
("dog" "sees" "bear" "+")
triple15
The cat does not like the bear.
False
1
inv-proof
[(triple9)]
("cat" "likes" "bear" "-")
triple9
The dog sees the dog.
True
2
proof
[(((triple14) -> rule4))]
("dog" "sees" "dog" "+")
((triple14) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The bear does not chase the bear.
False
2
inv-proof
[(((triple5) -> rule3))]
("bear" "chases" "bear" "-")
((triple5) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear is rough.
True
4
proof
[(((triple2 ((triple5) -> rule3)) -> rule6))]
("bear" "is" "rough" "+")
((triple2 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is not rough.
False
4
inv-proof
[(((triple2 ((triple5) -> rule3)) -> rule6))]
("bear" "is" "rough" "-")
((triple2 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is kind.
True
5
proof
[(((((triple2 ((triple5) -> rule3)) -> rule6)) -> rule1) OR ((((triple2 ((triple5) -> rule3)) -> rule6) triple3) -> rule2))]
("bear" "is" "kind" "+")
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The bear is not kind.
False
5
inv-proof
[(((((triple2 ((triple5) -> rule3)) -> rule6)) -> rule1) OR ((((triple2 ((triple5) -> rule3)) -> rule6) triple3) -> rule2))]
("bear" "is" "kind" "-")
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
The cat is not cold.
Unknown
inv-rconc
[@1: The cat is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("cat" "is" "cold" "-")
The cat sees the dog.
Unknown
rconc
[@1: The cat sees the dog.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("cat" "sees" "dog" "+")
The dog does not chase the bear.
Unknown
inv-rconc
[@1: The dog chases the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "chases" "bear" "-")
The dog is cold.
Unknown
rconc
[@1: The dog is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "is" "cold" "+")
The cat does not chase the cat.
Unknown
inv-random
[@0: The cat chases the cat.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "cat" "-")
The bear chases the dog.
Unknown
random
[@0: The bear chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("bear" "chases" "dog" "+")
The cat does not chase the dog.
Unknown
inv-random
[@0: The cat chases the dog.[CWA. Example of deepest failure = (FAIL)]]
("cat" "chases" "dog" "-")
The bear likes the bear.
Unknown
random
[@0: The bear likes the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "likes" "bear" "+")
@0: The bear is cold.[(triple1)] The bear is round.[(triple2)] The bear is young.[(triple3)] The bear likes the cat.[(triple4)] The bear likes the dog.[(triple5)] The bear sees the cat.[(triple6)] The bear sees the dog.[(triple7 OR ((triple4) -> rule4))] The cat chases the bear.[(triple8)] The cat likes the bear.[(triple9)] The dog does not chase the cat.[(triple10)] The dog is kind.[(triple11)] The dog is not young.[(triple12)] The dog likes the bear.[(triple13)] The dog likes the cat.[(triple14)] The dog sees the bear.[(triple15)] The dog sees the cat.[(triple16)] @1: The bear chases the bear.[(((triple5) -> rule3))] The dog sees the dog.[(((triple14) -> rule4))] @2: The bear is rough.[(((triple2 ((triple5) -> rule3)) -> rule6))] @3: The bear is kind.[(((((triple2 ((triple5) -> rule3)) -> rule6)) -> rule1) OR ((((triple2 ((triple5) -> rule3)) -> rule6) triple3) -> rule2))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is round.
("bear" "is" "round" "+")
triple2
The bear is young.
("bear" "is" "young" "+")
triple3
The bear likes the cat.
("bear" "likes" "cat" "+")
triple4
The bear likes the dog.
("bear" "likes" "dog" "+")
triple5
The bear sees the cat.
("bear" "sees" "cat" "+")
triple6
The bear sees the dog.
("bear" "sees" "dog" "+")
triple7
((triple4) -> (rule4 % int1))
The bear sees the dog.
("bear" "sees" "dog" "+")
int1
The cat chases the bear.
("cat" "chases" "bear" "+")
triple8
The cat likes the bear.
("cat" "likes" "bear" "+")
triple9
The dog does not chase the cat.
("dog" "chases" "cat" "-")
triple10
The dog is kind.
("dog" "is" "kind" "+")
triple11
The dog is not young.
("dog" "is" "young" "-")
triple12
The dog likes the bear.
("dog" "likes" "bear" "+")
triple13
The dog likes the cat.
("dog" "likes" "cat" "+")
triple14
The dog sees the bear.
("dog" "sees" "bear" "+")
triple15
The dog sees the cat.
("dog" "sees" "cat" "+")
triple16
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple5) -> (rule3 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The dog sees the dog.
("dog" "sees" "dog" "+")
((triple14) -> (rule4 % int1))
The dog sees the dog.
("dog" "sees" "dog" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
((triple2 ((triple5) -> (rule3 % int2))) -> (rule6 % int1))
The bear is rough.
("bear" "is" "rough" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear is kind.
("bear" "is" "kind" "+")
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2))) -> (rule1 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3
((((triple2 ((triple5) -> (rule3 % int3))) -> (rule6 % int2)) triple3) -> (rule2 % int1))
The bear is kind.
("bear" "is" "kind" "+")
int1
The bear is rough.
("bear" "is" "rough" "+")
int2
The bear chases the bear.
("bear" "chases" "bear" "+")
int3