The bear chases the cow. The cow is cold. The cow likes the dog. The cow sees the dog. The dog chases the bear. The dog is green. The dog is nice. The dog likes the bear. The dog sees the bear. The dog sees the cow. If something sees the cow and the cow is cold then the cow chases the dog. If something chases the bear and the bear chases the cow then the cow sees the dog. All big things are green. If something sees the dog and it chases the cow then the cow is green. If something likes the dog and it is big then the dog likes the cow. If something chases the dog then it is round. If something likes the dog and the dog chases the cow then it likes the bear. If something likes the dog and it sees the dog then it likes the cow.
The bear chases the cow.
("bear" "chases" "cow" "+")
The cow is cold.
("cow" "is" "cold" "+")
The cow likes the dog.
("cow" "likes" "dog" "+")
The cow sees the dog.
("cow" "sees" "dog" "+")
The dog chases the bear.
("dog" "chases" "bear" "+")
The dog is green.
("dog" "is" "green" "+")
The dog is nice.
("dog" "is" "nice" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog sees the bear.
("dog" "sees" "bear" "+")
The dog sees the cow.
("dog" "sees" "cow" "+")
If something sees the cow and the cow is cold then the cow chases the dog.
((("something" "sees" "cow" "+") ("cow" "is" "cold" "+")) -> ("cow" "chases" "dog" "+"))
If something chases the bear and the bear chases the cow then the cow sees the dog.
((("something" "chases" "bear" "+") ("bear" "chases" "cow" "+")) -> ("cow" "sees" "dog" "+"))
All big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If something sees the dog and it chases the cow then the cow is green.
((("something" "sees" "dog" "+") ("something" "chases" "cow" "+")) -> ("cow" "is" "green" "+"))
If something likes the dog and it is big then the dog likes the cow.
((("something" "likes" "dog" "+") ("something" "is" "big" "+")) -> ("dog" "likes" "cow" "+"))
If something chases the dog then it is round.
((("something" "chases" "dog" "+")) -> ("something" "is" "round" "+"))
If something likes the dog and the dog chases the cow then it likes the bear.
((("something" "likes" "dog" "+") ("dog" "chases" "cow" "+")) -> ("something" "likes" "bear" "+"))
If something likes the dog and it sees the dog then it likes the cow.
((("something" "likes" "dog" "+") ("something" "sees" "dog" "+")) -> ("something" "likes" "cow" "+"))
The dog sees the bear.
True
1
proof
[(triple9)]
("dog" "sees" "bear" "+")
triple9
The cow does not like the dog.
False
1
inv-proof
[(triple3)]
("cow" "likes" "dog" "-")
triple3
The cow likes the cow.
True
3
proof
[(((triple3 triple4) -> rule8) OR ((triple3 ((triple5 triple1) -> rule2)) -> rule8))]
("cow" "likes" "cow" "+")
((triple3 triple4) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((triple3 ((triple5 triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow does not chase the dog.
False
3
inv-proof
[(((triple10 triple2) -> rule1))]
("cow" "chases" "dog" "-")
((triple10 triple2) -> (rule1 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow is round.
True
4
proof
[(((((triple10 triple2) -> rule1)) -> rule6))]
("cow" "is" "round" "+")
((((triple10 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The cow is not round.
False
4
inv-proof
[(((((triple10 triple2) -> rule1)) -> rule6))]
("cow" "is" "round" "-")
((((triple10 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2
The bear is not round.
Unknown
inv-rconc
[@1: The bear is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("bear" "is" "round" "-")
The dog likes the cow.
Unknown
rconc
[@1: The dog likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("dog" "likes" "cow" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("dog" "is" "round" "-")
The bear sees the bear.
Unknown
random
[@0: The bear sees the bear.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "bear" "+")
The cow does not chase the bear.
Unknown
inv-random
[@0: The cow chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("cow" "chases" "bear" "-")
The dog likes the dog.
Unknown
random
[@0: The dog likes the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "likes" "dog" "+")
@0: The bear chases the cow.[(triple1)] The cow is cold.[(triple2)] The cow likes the dog.[(triple3)] The cow sees the dog.[(triple4 OR ((triple5 triple1) -> rule2))] The dog chases the bear.[(triple5)] The dog is green.[(triple6)] The dog is nice.[(triple7)] The dog likes the bear.[(triple8)] The dog sees the bear.[(triple9)] The dog sees the cow.[(triple10)] @1: The cow chases the dog.[(((triple10 triple2) -> rule1))] The cow likes the cow.[(((triple3 triple4) -> rule8) OR ((triple3 ((triple5 triple1) -> rule2)) -> rule8))] @2: The cow is round.[(((((triple10 triple2) -> rule1)) -> rule6))]
The bear chases the cow.
("bear" "chases" "cow" "+")
triple1
The cow is cold.
("cow" "is" "cold" "+")
triple2
The cow likes the dog.
("cow" "likes" "dog" "+")
triple3
The cow sees the dog.
("cow" "sees" "dog" "+")
triple4
((triple5 triple1) -> (rule2 % int1))
The cow sees the dog.
("cow" "sees" "dog" "+")
int1
The dog chases the bear.
("dog" "chases" "bear" "+")
triple5
The dog is green.
("dog" "is" "green" "+")
triple6
The dog is nice.
("dog" "is" "nice" "+")
triple7
The dog likes the bear.
("dog" "likes" "bear" "+")
triple8
The dog sees the bear.
("dog" "sees" "bear" "+")
triple9
The dog sees the cow.
("dog" "sees" "cow" "+")
triple10
The cow chases the dog.
("cow" "chases" "dog" "+")
((triple10 triple2) -> (rule1 % int1))
The cow chases the dog.
("cow" "chases" "dog" "+")
int1
The cow likes the cow.
("cow" "likes" "cow" "+")
((triple3 triple4) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
((triple3 ((triple5 triple1) -> (rule2 % int2))) -> (rule8 % int1))
The cow likes the cow.
("cow" "likes" "cow" "+")
int1
The cow sees the dog.
("cow" "sees" "dog" "+")
int2
The cow is round.
("cow" "is" "round" "+")
((((triple10 triple2) -> (rule1 % int2))) -> (rule6 % int1))
The cow is round.
("cow" "is" "round" "+")
int1
The cow chases the dog.
("cow" "chases" "dog" "+")
int2