Anne is blue. Bob is green. Fiona is big. If someone is green then they are blue. If someone is blue then they are cold. If Bob is big then Bob is green. Green, kind people are blue. Big people are green. If Anne is green and Anne is cold then Anne is kind.
Anne is blue.
("Anne" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Fiona is big.
("Fiona" "is" "big" "+")
If someone is green then they are blue.
((("someone" "is" "green" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue then they are cold.
((("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
If Bob is big then Bob is green.
((("Bob" "is" "big" "+")) -> ("Bob" "is" "green" "+"))
Green, kind people are blue.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "blue" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
If Anne is green and Anne is cold then Anne is kind.
((("Anne" "is" "green" "+") ("Anne" "is" "cold" "+")) -> ("Anne" "is" "kind" "+"))
Bob is green.
True
1
proof
[(triple2)]
("Bob" "is" "green" "+")
triple2
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Bob is blue.
True
2
proof
[(((triple2) -> rule1))]
("Bob" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Fiona is blue.
True
3
proof
[(((((triple3) -> rule5)) -> rule1))]
("Fiona" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not blue.
False
3
inv-proof
[(((((triple3) -> rule5)) -> rule1))]
("Fiona" "is" "blue" "-")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is kind.
Unknown
rconc
[@2: Anne is kind.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Anne" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Anne is smart.
Unknown
random
[@0: Anne is smart.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "smart" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Anne is blue.[(triple1)] Bob is green.[(triple2)] Fiona is big.[(triple3)] @1: Anne is cold.[(((triple1) -> rule2))] Bob is blue.[(((triple2) -> rule1))] Fiona is green.[(((triple3) -> rule5))] @2: Bob is cold.[(((((triple2) -> rule1)) -> rule2))] Fiona is blue.[(((((triple3) -> rule5)) -> rule1))] @3: Fiona is cold.[(((((((triple3) -> rule5)) -> rule1)) -> rule2))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Fiona is big.
("Fiona" "is" "big" "+")
triple3
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple3) -> (rule5 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple3) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple3) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
int3