Anne is big. Bob is rough. Erin is not white. If Anne is not big then Anne is blue. If something is big and not rough then it is green. Blue things are green. If something is white and blue then it is not green. All blue things are white. Big things are white. If something is white and big then it is not kind. All kind things are round.
Anne is big.
("Anne" "is" "big" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is not white.
("Erin" "is" "white" "-")
If Anne is not big then Anne is blue.
((("Anne" "is" "big" "~")) -> ("Anne" "is" "blue" "+"))
If something is big and not rough then it is green.
((("something" "is" "big" "+") ("something" "is" "rough" "~")) -> ("something" "is" "green" "+"))
Blue things are green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "+"))
If something is white and blue then it is not green.
((("something" "is" "white" "+") ("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
All blue things are white.
((("something" "is" "blue" "+")) -> ("something" "is" "white" "+"))
Big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
If something is white and big then it is not kind.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "-"))
All kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Bob is rough.
True
1
proof
[(triple2)]
("Bob" "is" "rough" "+")
triple2
Anne is not big.
False
1
inv-proof
[(triple1)]
("Anne" "is" "big" "-")
triple1
Anne is white.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not white.
False
2
inv-proof
[(((triple1) -> rule6))]
("Anne" "is" "white" "-")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not kind.
True
4
proof
[(((((triple1) -> rule6) triple1) -> rule7))]
("Anne" "is" "kind" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Anne is kind.
False
4
inv-proof
[(((((triple1) -> rule6) triple1) -> rule7))]
("Anne" "is" "kind" "+")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2
Erin is not round.
Unknown
inv-rconc
[@1: Erin is round.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Erin" "is" "round" "-")
Anne is green.
Unknown
rconc
[@2: Anne is green.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Anne" "is" "green" "+")
Anne is not blue.
Unknown
inv-rconc
[@1: Anne is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "blue" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Anne is big.[(triple1)] Bob is rough.[(triple2)] Erin is not white.[(triple3)] @1: Anne is white.[(((triple1) -> rule6))] @2: Anne is not kind.[(((((triple1) -> rule6) triple1) -> rule7))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Erin is not white.
("Erin" "is" "white" "-")
triple3
Anne is white.
("Anne" "is" "white" "+")
((triple1) -> (rule6 % int1))
Anne is white.
("Anne" "is" "white" "+")
int1
Anne is not kind.
("Anne" "is" "kind" "-")
((((triple1) -> (rule6 % int2)) triple1) -> (rule7 % int1))
Anne is not kind.
("Anne" "is" "kind" "-")
int1
Anne is white.
("Anne" "is" "white" "+")
int2