The bear is cold. The bear is green. The bear visits the rabbit. The cow likes the rabbit. The dog is green. The dog likes the bear. The dog likes the cow. The rabbit is cold. The rabbit is green. The rabbit likes the cow. The rabbit needs the cow. The rabbit visits the dog. If something needs the cow and it is cold then the cow needs the bear. If the bear is green then the bear likes the rabbit. If something likes the dog and the dog likes the rabbit then the dog is round. If something needs the bear then it visits the cow. If something needs the dog and the dog visits the cow then it likes the cow. If something visits the cow then the cow is big.
The bear is cold.
("bear" "is" "cold" "+")
The bear is green.
("bear" "is" "green" "+")
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
The dog is green.
("dog" "is" "green" "+")
The dog likes the bear.
("dog" "likes" "bear" "+")
The dog likes the cow.
("dog" "likes" "cow" "+")
The rabbit is cold.
("rabbit" "is" "cold" "+")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
If something needs the cow and it is cold then the cow needs the bear.
((("something" "needs" "cow" "+") ("something" "is" "cold" "+")) -> ("cow" "needs" "bear" "+"))
If the bear is green then the bear likes the rabbit.
((("bear" "is" "green" "+")) -> ("bear" "likes" "rabbit" "+"))
If something likes the dog and the dog likes the rabbit then the dog is round.
((("something" "likes" "dog" "+") ("dog" "likes" "rabbit" "+")) -> ("dog" "is" "round" "+"))
If something needs the bear then it visits the cow.
((("something" "needs" "bear" "+")) -> ("something" "visits" "cow" "+"))
If something needs the dog and the dog visits the cow then it likes the cow.
((("something" "needs" "dog" "+") ("dog" "visits" "cow" "+")) -> ("something" "likes" "cow" "+"))
If something visits the cow then the cow is big.
((("something" "visits" "cow" "+")) -> ("cow" "is" "big" "+"))
The rabbit is green.
True
1
proof
[(triple9)]
("rabbit" "is" "green" "+")
triple9
The bear is not green.
False
1
inv-proof
[(triple2)]
("bear" "is" "green" "-")
triple2
The cow needs the bear.
True
3
proof
[(((triple11 triple8) -> rule1))]
("cow" "needs" "bear" "+")
((triple11 triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow does not need the bear.
False
3
inv-proof
[(((triple11 triple8) -> rule1))]
("cow" "needs" "bear" "-")
((triple11 triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow visits the cow.
True
4
proof
[(((((triple11 triple8) -> rule1)) -> rule4))]
("cow" "visits" "cow" "+")
((((triple11 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow does not visit the cow.
False
4
inv-proof
[(((((triple11 triple8) -> rule1)) -> rule4))]
("cow" "visits" "cow" "-")
((((triple11 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow is big.
True
5
proof
[(((((((triple11 triple8) -> rule1)) -> rule4)) -> rule6))]
("cow" "is" "big" "+")
((((((triple11 triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
The cow is not big.
False
5
inv-proof
[(((((((triple11 triple8) -> rule1)) -> rule4)) -> rule6))]
("cow" "is" "big" "-")
((((((triple11 triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3
The rabbit does not visit the cow.
Unknown
inv-rconc
[@1: The rabbit visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("rabbit" "visits" "cow" "-")
The bear likes the cow.
Unknown
rconc
[@1: The bear likes the cow.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("bear" "likes" "cow" "+")
The dog is not round.
Unknown
inv-rconc
[@1: The dog is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("dog" "is" "round" "-")
The dog visits the cow.
Unknown
rconc
[@1: The dog visits the cow.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("dog" "visits" "cow" "+")
The dog does not need the cow.
Unknown
inv-random
[@0: The dog needs the cow.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "cow" "-")
The rabbit needs the bear.
Unknown
random
[@0: The rabbit needs the bear.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "needs" "bear" "+")
The dog does not need the dog.
Unknown
inv-random
[@0: The dog needs the dog.[CWA. Example of deepest failure = (FAIL)]]
("dog" "needs" "dog" "-")
The cow visits the dog.
Unknown
random
[@0: The cow visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("cow" "visits" "dog" "+")
@0: The bear is cold.[(triple1)] The bear is green.[(triple2)] The bear visits the rabbit.[(triple3)] The cow likes the rabbit.[(triple4)] The dog is green.[(triple5)] The dog likes the bear.[(triple6)] The dog likes the cow.[(triple7)] The rabbit is cold.[(triple8)] The rabbit is green.[(triple9)] The rabbit likes the cow.[(triple10)] The rabbit needs the cow.[(triple11)] The rabbit visits the dog.[(triple12)] @1: The bear likes the rabbit.[(((triple2) -> rule2))] The cow needs the bear.[(((triple11 triple8) -> rule1))] @2: The cow visits the cow.[(((((triple11 triple8) -> rule1)) -> rule4))] @3: The cow is big.[(((((((triple11 triple8) -> rule1)) -> rule4)) -> rule6))]
The bear is cold.
("bear" "is" "cold" "+")
triple1
The bear is green.
("bear" "is" "green" "+")
triple2
The bear visits the rabbit.
("bear" "visits" "rabbit" "+")
triple3
The cow likes the rabbit.
("cow" "likes" "rabbit" "+")
triple4
The dog is green.
("dog" "is" "green" "+")
triple5
The dog likes the bear.
("dog" "likes" "bear" "+")
triple6
The dog likes the cow.
("dog" "likes" "cow" "+")
triple7
The rabbit is cold.
("rabbit" "is" "cold" "+")
triple8
The rabbit is green.
("rabbit" "is" "green" "+")
triple9
The rabbit likes the cow.
("rabbit" "likes" "cow" "+")
triple10
The rabbit needs the cow.
("rabbit" "needs" "cow" "+")
triple11
The rabbit visits the dog.
("rabbit" "visits" "dog" "+")
triple12
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
((triple2) -> (rule2 % int1))
The bear likes the rabbit.
("bear" "likes" "rabbit" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
((triple11 triple8) -> (rule1 % int1))
The cow needs the bear.
("cow" "needs" "bear" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
((((triple11 triple8) -> (rule1 % int2))) -> (rule4 % int1))
The cow visits the cow.
("cow" "visits" "cow" "+")
int1
The cow needs the bear.
("cow" "needs" "bear" "+")
int2
The cow is big.
("cow" "is" "big" "+")
((((((triple11 triple8) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
The cow is big.
("cow" "is" "big" "+")
int1
The cow visits the cow.
("cow" "visits" "cow" "+")
int2
The cow needs the bear.
("cow" "needs" "bear" "+")
int3