The cow is round. The cow visits the tiger. The dog chases the tiger. The dog is round. The dog is young. The dog visits the cow. The dog does not visit the rabbit. The rabbit is green. The rabbit is round. The tiger visits the dog. If something visits the tiger then the tiger needs the cow. If something is green and it needs the tiger then it is young. If something needs the cow then the cow needs the tiger.
The cow is round.
("cow" "is" "round" "+")
The cow visits the tiger.
("cow" "visits" "tiger" "+")
The dog chases the tiger.
("dog" "chases" "tiger" "+")
The dog is round.
("dog" "is" "round" "+")
The dog is young.
("dog" "is" "young" "+")
The dog visits the cow.
("dog" "visits" "cow" "+")
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
The rabbit is green.
("rabbit" "is" "green" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The tiger visits the dog.
("tiger" "visits" "dog" "+")
If something visits the tiger then the tiger needs the cow.
((("something" "visits" "tiger" "+")) -> ("tiger" "needs" "cow" "+"))
If something is green and it needs the tiger then it is young.
((("something" "is" "green" "+") ("something" "needs" "tiger" "+")) -> ("something" "is" "young" "+"))
If something needs the cow then the cow needs the tiger.
((("something" "needs" "cow" "+")) -> ("cow" "needs" "tiger" "+"))
The cow visits the tiger.
True
1
proof
[(triple2)]
("cow" "visits" "tiger" "+")
triple2
The cow does not visit the tiger.
False
1
inv-proof
[(triple2)]
("cow" "visits" "tiger" "-")
triple2
The tiger needs the cow.
True
2
proof
[(((triple2) -> rule1))]
("tiger" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The tiger does not need the cow.
False
2
inv-proof
[(((triple2) -> rule1))]
("tiger" "needs" "cow" "-")
((triple2) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow needs the tiger.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "needs" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The cow does not need the tiger.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule3))]
("cow" "needs" "tiger" "-")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2
The rabbit is not young.
Unknown
inv-rconc
[@1: The rabbit is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "is" "young" "-")
The cow is young.
Unknown
rconc
[@1: The cow is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("cow" "is" "young" "+")
The tiger is not young.
Unknown
inv-rconc
[@1: The tiger is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("tiger" "is" "young" "-")
The rabbit is kind.
Unknown
random
[@0: The rabbit is kind.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "is" "kind" "+")
The dog is not rough.
Unknown
inv-random
[@0: The dog is rough.[CWA. Example of deepest failure = (FAIL)]]
("dog" "is" "rough" "-")
The rabbit visits the dog.
Unknown
random
[@0: The rabbit visits the dog.[CWA. Example of deepest failure = (FAIL)]]
("rabbit" "visits" "dog" "+")
@0: The cow is round.[(triple1)] The cow visits the tiger.[(triple2)] The dog chases the tiger.[(triple3)] The dog does not visit the rabbit.[(triple7)] The dog is round.[(triple4)] The dog is young.[(triple5)] The dog visits the cow.[(triple6)] The rabbit is green.[(triple8)] The rabbit is round.[(triple9)] The tiger visits the dog.[(triple10)] @1: The tiger needs the cow.[(((triple2) -> rule1))] @2: The cow needs the tiger.[(((((triple2) -> rule1)) -> rule3))]
The cow is round.
("cow" "is" "round" "+")
triple1
The cow visits the tiger.
("cow" "visits" "tiger" "+")
triple2
The dog chases the tiger.
("dog" "chases" "tiger" "+")
triple3
The dog does not visit the rabbit.
("dog" "visits" "rabbit" "-")
triple7
The dog is round.
("dog" "is" "round" "+")
triple4
The dog is young.
("dog" "is" "young" "+")
triple5
The dog visits the cow.
("dog" "visits" "cow" "+")
triple6
The rabbit is green.
("rabbit" "is" "green" "+")
triple8
The rabbit is round.
("rabbit" "is" "round" "+")
triple9
The tiger visits the dog.
("tiger" "visits" "dog" "+")
triple10
The tiger needs the cow.
("tiger" "needs" "cow" "+")
((triple2) -> (rule1 % int1))
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int1
The cow needs the tiger.
("cow" "needs" "tiger" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
The cow needs the tiger.
("cow" "needs" "tiger" "+")
int1
The tiger needs the cow.
("tiger" "needs" "cow" "+")
int2