The bear chases the cat. The bear chases the rabbit. The bear is nice. The bear sees the rabbit. The cat chases the bear. The cat chases the rabbit. The cat is blue. The cat sees the rabbit. The cat sees the tiger. The rabbit chases the cat. The rabbit chases the tiger. The rabbit is round. The rabbit visits the bear. The tiger is round. The tiger sees the rabbit. If something is nice then it sees the cat. If something is nice and it sees the cat then it chases the bear.
The bear chases the cat.
("bear" "chases" "cat" "+")
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
The bear is nice.
("bear" "is" "nice" "+")
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
The cat chases the bear.
("cat" "chases" "bear" "+")
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
The cat is blue.
("cat" "is" "blue" "+")
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
The cat sees the tiger.
("cat" "sees" "tiger" "+")
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
The rabbit is round.
("rabbit" "is" "round" "+")
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
The tiger is round.
("tiger" "is" "round" "+")
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
If something is nice then it sees the cat.
((("something" "is" "nice" "+")) -> ("something" "sees" "cat" "+"))
If something is nice and it sees the cat then it chases the bear.
((("something" "is" "nice" "+") ("something" "sees" "cat" "+")) -> ("something" "chases" "bear" "+"))
The tiger sees the rabbit.
True
1
proof
[(triple15)]
("tiger" "sees" "rabbit" "+")
triple15
The rabbit does not chase the cat.
False
1
inv-proof
[(triple10)]
("rabbit" "chases" "cat" "-")
triple10
The bear sees the cat.
True
2
proof
[(((triple3) -> rule1))]
("bear" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear does not see the cat.
False
2
inv-proof
[(((triple3) -> rule1))]
("bear" "sees" "cat" "-")
((triple3) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear chases the bear.
True
4
proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("bear" "chases" "bear" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The bear does not chase the bear.
False
4
inv-proof
[(((triple3 ((triple3) -> rule1)) -> rule2))]
("bear" "chases" "bear" "-")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2
The cat does not see the cat.
Unknown
inv-rconc
[@1: The cat sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("cat" "sees" "cat" "-")
The rabbit chases the bear.
Unknown
rconc
[@1: The rabbit chases the bear.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("rabbit" "chases" "bear" "+")
The rabbit does not see the cat.
Unknown
inv-rconc
[@1: The rabbit sees the cat.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("rabbit" "sees" "cat" "-")
The bear sees the tiger.
Unknown
random
[@0: The bear sees the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "sees" "tiger" "+")
The tiger does not visit the bear.
Unknown
inv-random
[@0: The tiger visits the bear.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "visits" "bear" "-")
The tiger is rough.
Unknown
random
[@0: The tiger is rough.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "rough" "+")
@0: The bear chases the cat.[(triple1)] The bear chases the rabbit.[(triple2)] The bear is nice.[(triple3)] The bear sees the rabbit.[(triple4)] The cat chases the bear.[(triple5)] The cat chases the rabbit.[(triple6)] The cat is blue.[(triple7)] The cat sees the rabbit.[(triple8)] The cat sees the tiger.[(triple9)] The rabbit chases the cat.[(triple10)] The rabbit chases the tiger.[(triple11)] The rabbit is round.[(triple12)] The rabbit visits the bear.[(triple13)] The tiger is round.[(triple14)] The tiger sees the rabbit.[(triple15)] @1: The bear sees the cat.[(((triple3) -> rule1))] @2: The bear chases the bear.[(((triple3 ((triple3) -> rule1)) -> rule2))]
The bear chases the cat.
("bear" "chases" "cat" "+")
triple1
The bear chases the rabbit.
("bear" "chases" "rabbit" "+")
triple2
The bear is nice.
("bear" "is" "nice" "+")
triple3
The bear sees the rabbit.
("bear" "sees" "rabbit" "+")
triple4
The cat chases the bear.
("cat" "chases" "bear" "+")
triple5
The cat chases the rabbit.
("cat" "chases" "rabbit" "+")
triple6
The cat is blue.
("cat" "is" "blue" "+")
triple7
The cat sees the rabbit.
("cat" "sees" "rabbit" "+")
triple8
The cat sees the tiger.
("cat" "sees" "tiger" "+")
triple9
The rabbit chases the cat.
("rabbit" "chases" "cat" "+")
triple10
The rabbit chases the tiger.
("rabbit" "chases" "tiger" "+")
triple11
The rabbit is round.
("rabbit" "is" "round" "+")
triple12
The rabbit visits the bear.
("rabbit" "visits" "bear" "+")
triple13
The tiger is round.
("tiger" "is" "round" "+")
triple14
The tiger sees the rabbit.
("tiger" "sees" "rabbit" "+")
triple15
The bear sees the cat.
("bear" "sees" "cat" "+")
((triple3) -> (rule1 % int1))
The bear sees the cat.
("bear" "sees" "cat" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((triple3 ((triple3) -> (rule1 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear sees the cat.
("bear" "sees" "cat" "+")
int2