Anne is white. Bob is cold. Charlie is nice. Erin is green. If someone is red and not cold then they are nice. Young people are nice. All red people are nice. If Anne is cold and Anne is not young then Anne is red. If Anne is young and Anne is blue then Anne is nice. If Bob is cold and Bob is not nice then Bob is green. All green people are white. If someone is cold and not green then they are not white.
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Erin is green.
("Erin" "is" "green" "+")
If someone is red and not cold then they are nice.
((("someone" "is" "red" "+") ("someone" "is" "cold" "~")) -> ("someone" "is" "nice" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All red people are nice.
((("someone" "is" "red" "+")) -> ("someone" "is" "nice" "+"))
If Anne is cold and Anne is not young then Anne is red.
((("Anne" "is" "cold" "+") ("Anne" "is" "young" "~")) -> ("Anne" "is" "red" "+"))
If Anne is young and Anne is blue then Anne is nice.
((("Anne" "is" "young" "+") ("Anne" "is" "blue" "+")) -> ("Anne" "is" "nice" "+"))
If Bob is cold and Bob is not nice then Bob is green.
((("Bob" "is" "cold" "+") ("Bob" "is" "nice" "~")) -> ("Bob" "is" "green" "+"))
All green people are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is cold and not green then they are not white.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "white" "-"))
Erin is green.
True
1
proof
[(triple4)]
("Erin" "is" "green" "+")
triple4
Charlie is not nice.
False
1
inv-proof
[(triple3)]
("Charlie" "is" "nice" "-")
triple3
Erin is white.
True
2
proof
[(((triple4) -> rule7))]
("Erin" "is" "white" "+")
((triple4) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is not white.
False
2
inv-proof
[(((triple4) -> rule7))]
("Erin" "is" "white" "-")
((triple4) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "white" "-")
Bob is white.
Unknown
rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule7 <- rule6 <- FAIL)]]
("Bob" "is" "white" "+")
Anne is not cold.
Unknown
inv-random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is white.[(triple1)] Bob is cold.[(triple2)] Charlie is nice.[(triple3)] Erin is green.[(triple4)] @1: Erin is white.[(((triple4) -> rule7))]
Anne is white.
("Anne" "is" "white" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
triple4
Erin is white.
("Erin" "is" "white" "+")
((triple4) -> (rule7 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1