The bear chases the tiger. The bear is blue. The tiger is not red. If something chases the bear then the bear needs the tiger. If something visits the bear then it chases the bear. If something is blue then it visits the bear.
The bear chases the tiger.
("bear" "chases" "tiger" "+")
The bear is blue.
("bear" "is" "blue" "+")
The tiger is not red.
("tiger" "is" "red" "-")
If something chases the bear then the bear needs the tiger.
((("something" "chases" "bear" "+")) -> ("bear" "needs" "tiger" "+"))
If something visits the bear then it chases the bear.
((("something" "visits" "bear" "+")) -> ("something" "chases" "bear" "+"))
If something is blue then it visits the bear.
((("something" "is" "blue" "+")) -> ("something" "visits" "bear" "+"))
The bear is blue.
True
1
proof
[(triple2)]
("bear" "is" "blue" "+")
triple2
The tiger is red.
False
1
inv-proof
[(triple3)]
("tiger" "is" "red" "+")
triple3
The bear visits the bear.
True
2
proof
[(((triple2) -> rule3))]
("bear" "visits" "bear" "+")
((triple2) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear does not visit the bear.
False
2
inv-proof
[(((triple2) -> rule3))]
("bear" "visits" "bear" "-")
((triple2) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear chases the bear.
True
3
proof
[(((((triple2) -> rule3)) -> rule2))]
("bear" "chases" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear does not chase the bear.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule2))]
("bear" "chases" "bear" "-")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The tiger does not chase the bear.
Unknown
inv-rconc
[@2: The tiger chases the bear.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("tiger" "chases" "bear" "-")
The tiger visits the bear.
Unknown
rconc
[@1: The tiger visits the bear.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("tiger" "visits" "bear" "+")
The tiger does not need the tiger.
Unknown
inv-random
[@0: The tiger needs the tiger.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "needs" "tiger" "-")
The tiger is cold.
Unknown
random
[@0: The tiger is cold.[CWA. Example of deepest failure = (FAIL)]]
("tiger" "is" "cold" "+")
The bear does not visit the tiger.
Unknown
inv-random
[@0: The bear visits the tiger.[CWA. Example of deepest failure = (FAIL)]]
("bear" "visits" "tiger" "-")
The bear is cold.
Unknown
random
[@0: The bear is cold.[CWA. Example of deepest failure = (FAIL)]]
("bear" "is" "cold" "+")
@0: The bear chases the tiger.[(triple1)] The bear is blue.[(triple2)] The tiger is not red.[(triple3)] @1: The bear visits the bear.[(((triple2) -> rule3))] @2: The bear chases the bear.[(((((triple2) -> rule3)) -> rule2))] @3: The bear needs the tiger.[(((((((triple2) -> rule3)) -> rule2)) -> rule1))]
The bear chases the tiger.
("bear" "chases" "tiger" "+")
triple1
The bear is blue.
("bear" "is" "blue" "+")
triple2
The tiger is not red.
("tiger" "is" "red" "-")
triple3
The bear visits the bear.
("bear" "visits" "bear" "+")
((triple2) -> (rule3 % int1))
The bear visits the bear.
("bear" "visits" "bear" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
((((triple2) -> (rule3 % int2))) -> (rule2 % int1))
The bear chases the bear.
("bear" "chases" "bear" "+")
int1
The bear visits the bear.
("bear" "visits" "bear" "+")
int2
The bear needs the tiger.
("bear" "needs" "tiger" "+")
((((((triple2) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
The bear needs the tiger.
("bear" "needs" "tiger" "+")
int1
The bear chases the bear.
("bear" "chases" "bear" "+")
int2
The bear visits the bear.
("bear" "visits" "bear" "+")
int3