The bear chases the tiger. The bear is red. The bear sees the cow. The bear visits the cow. The bear visits the tiger. The cow chases the dog. The cow chases the tiger. The cow sees the bear. The cow visits the bear. The cow visits the dog. The dog chases the cow. The dog chases the tiger. The dog visits the cow. The dog visits the tiger. The tiger visits the bear. All cold things are nice. If something is rough then it visits the tiger. If something chases the cow and it sees the tiger then it sees the cow. If something is rough then it sees the dog. If the tiger chases the bear and the tiger visits the dog then the bear sees the cow. If something chases the dog then it sees the cow. If something visits the cow then the cow chases the tiger. If something sees the bear then the bear chases the tiger.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is red.
("bear" "is" "red" "+")
The bear sees the cow.
("bear" "sees" "cow" "+")
The bear visits the cow.
("bear" "visits" "cow" "+")
The bear visits the tiger.
("bear" "visits" "tiger" "+")
The cow chases the dog.
("cow" "chases" "dog" "+")
The cow chases the tiger.
("cow" "chases" "tiger" "+")
The cow sees the bear.
("cow" "sees" "bear" "+")
The cow visits the bear.
("cow" "visits" "bear" "+")
The cow visits the dog.
("cow" "visits" "dog" "+")
The dog chases the cow.
("dog" "chases" "cow" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog visits the tiger.
("dog" "visits" "tiger" "+")
The tiger visits the bear.
("tiger" "visits" "bear" "+")
All cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
If something is rough then it visits the tiger.
((("something" "is" "rough" "+")) -> ("something" "visits" "tiger" "+"))
If something chases the cow and it sees the tiger then it sees the cow.
((("something" "chases" "cow" "+") ("something" "sees" "tiger" "+")) -> ("something" "sees" "cow" "+"))
If something is rough then it sees the dog.
((("something" "is" "rough" "+")) -> ("something" "sees" "dog" "+"))
If the tiger chases the bear and the tiger visits the dog then the bear sees the cow.
((("tiger" "chases" "bear" "+") ("tiger" "visits" "dog" "+")) -> ("bear" "sees" "cow" "+"))
If something chases the dog then it sees the cow.
((("something" "chases" "dog" "+")) -> ("something" "sees" "cow" "+"))
If something visits the cow then the cow chases the tiger.
((("something" "visits" "cow" "+")) -> ("cow" "chases" "tiger" "+"))
If something sees the bear then the bear chases the tiger.
((("something" "sees" "bear" "+")) -> ("bear" "chases" "tiger" "+"))
The bear visits the cow.
True
1
proof
[(triple4)]
("bear" "visits" "cow" "+")
triple4
The bear does not visit the tiger.
False
1
inv-proof
[(triple5)]
("bear" "visits" "tiger" "-")
triple5
The cow sees the cow.
True
2
proof
[(((triple6) -> rule6))]
("cow" "sees" "cow" "+")
((triple6) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The cow does not see the cow.
False
2
inv-proof
[(((triple6) -> rule6))]
("cow" "sees" "cow" "-")
((triple6) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1
The dog does not see the cow.
Unknown
inv-rconc
[@1: The dog sees the cow.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "sees" "cow" "-")
The dog is nice.
Unknown
rconc
[@1: The dog is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("dog" "is" "nice" "+")
The cow is not rough.
Unknown
inv-random
[@0: The cow is rough.[CWA. Example of deepest failure = (FAIL)]]
("cow" "is" "rough" "-")
The tiger chases the bear.
Unknown
random
[@0: The tiger chases the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "chases" "bear" "+")
@0: The bear chases the tiger.[(triple1 OR ((triple8) -> rule8))] The bear is red.[(triple2)] The bear sees the cow.[(triple3)] The bear visits the cow.[(triple4)] The bear visits the tiger.[(triple5)] The cow chases the dog.[(triple6)] The cow chases the tiger.[(triple7 OR ((triple13) -> rule7) OR ((triple4) -> rule7))] The cow sees the bear.[(triple8)] The cow visits the bear.[(triple9)] The cow visits the dog.[(triple10)] The dog chases the cow.[(triple11)] The dog chases the tiger.[(triple12)] The dog visits the cow.[(triple13)] The dog visits the tiger.[(triple14)] The tiger visits the bear.[(triple15)] @1: The cow sees the cow.[(((triple6) -> rule6))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
((triple8) -> (rule8 % int1))
The bear chases the tiger.
("bear" "chases" "tiger" "+")
int1
The bear is red.
("bear" "is" "red" "+")
triple2
The bear sees the cow.
("bear" "sees" "cow" "+")
triple3
The bear visits the cow.
("bear" "visits" "cow" "+")
triple4
The bear visits the tiger.
("bear" "visits" "tiger" "+")
triple5
The cow chases the dog.
("cow" "chases" "dog" "+")
triple6
The cow chases the tiger.
("cow" "chases" "tiger" "+")
triple7
((triple13) -> (rule7 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
((triple4) -> (rule7 % int1))
The cow chases the tiger.
("cow" "chases" "tiger" "+")
int1
The cow sees the bear.
("cow" "sees" "bear" "+")
triple8
The cow visits the bear.
("cow" "visits" "bear" "+")
triple9
The cow visits the dog.
("cow" "visits" "dog" "+")
triple10
The dog chases the cow.
("dog" "chases" "cow" "+")
triple11
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple12
The dog visits the cow.
("dog" "visits" "cow" "+")
triple13
The dog visits the tiger.
("dog" "visits" "tiger" "+")
triple14
The tiger visits the bear.
("tiger" "visits" "bear" "+")
triple15
The cow sees the cow.
("cow" "sees" "cow" "+")
((triple6) -> (rule6 % int1))
The cow sees the cow.
("cow" "sees" "cow" "+")
int1