Bob is red. Red, green people are cold. If Bob is nice then Bob is quiet. If someone is red and cold then they are big. If someone is red then they are green. If someone is nice and not red then they are rough. If someone is quiet and not green then they are rough.
Bob is red.
("Bob" "is" "red" "+")
Red, green people are cold.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "cold" "+"))
If Bob is nice then Bob is quiet.
((("Bob" "is" "nice" "+")) -> ("Bob" "is" "quiet" "+"))
If someone is red and cold then they are big.
((("someone" "is" "red" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
If someone is red then they are green.
((("someone" "is" "red" "+")) -> ("someone" "is" "green" "+"))
If someone is nice and not red then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "red" "~")) -> ("someone" "is" "rough" "+"))
If someone is quiet and not green then they are rough.
((("someone" "is" "quiet" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "rough" "+"))
Bob is red.
True
1
proof
[(triple1)]
("Bob" "is" "red" "+")
triple1
Bob is not red.
False
1
inv-proof
[(triple1)]
("Bob" "is" "red" "-")
triple1
Bob is green.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule4))]
("Bob" "is" "green" "-")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
True
4
proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((triple1 ((triple1) -> rule4)) -> rule1))]
("Bob" "is" "cold" "-")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "rough" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is red.[(triple1)] @1: Bob is green.[(((triple1) -> rule4))] @2: Bob is cold.[(((triple1 ((triple1) -> rule4)) -> rule1))] @3: Bob is big.[(((triple1 ((triple1 ((triple1) -> rule4)) -> rule1)) -> rule3))]
Bob is red.
("Bob" "is" "red" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((triple1 ((triple1) -> (rule4 % int2))) -> (rule1 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple1 ((triple1 ((triple1) -> (rule4 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3