Dave is white. Erin is green. Erin is kind. All round people are green. Kind, cold people are green. If someone is round then they are not green. All green, kind people are cold. If Erin is cold then Erin is white. If someone is green and not kind then they are nice. If Erin is not green then Erin is not young. If someone is white and not nice then they are young.
Dave is white.
("Dave" "is" "white" "+")
Erin is green.
("Erin" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
All round people are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
Kind, cold people are green.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "+"))
If someone is round then they are not green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "-"))
All green, kind people are cold.
((("someone" "is" "green" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If Erin is cold then Erin is white.
((("Erin" "is" "cold" "+")) -> ("Erin" "is" "white" "+"))
If someone is green and not kind then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "kind" "~")) -> ("someone" "is" "nice" "+"))
If Erin is not green then Erin is not young.
((("Erin" "is" "green" "~")) -> ("Erin" "is" "young" "-"))
If someone is white and not nice then they are young.
((("someone" "is" "white" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "young" "+"))
Erin is green.
True
1
proof
[(triple2)]
("Erin" "is" "green" "+")
triple2
Dave is not white.
False
1
inv-proof
[(triple1)]
("Dave" "is" "white" "-")
triple1
Erin is cold.
True
3
proof
[(((triple2 triple3) -> rule4))]
("Erin" "is" "cold" "+")
((triple2 triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is not cold.
False
3
inv-proof
[(((triple2 triple3) -> rule4))]
("Erin" "is" "cold" "-")
((triple2 triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
True
4
proof
[(((((triple2 triple3) -> rule4)) -> rule5))]
("Erin" "is" "white" "+")
((((triple2 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Erin is not white.
False
4
inv-proof
[(((((triple2 triple3) -> rule4)) -> rule5))]
("Erin" "is" "white" "-")
((((triple2 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Dave is nice.
Unknown
rconc
[@1: Dave is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "nice" "+")
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is round.
Unknown
random
[@0: Dave is round.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "round" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Erin is round.
Unknown
random
[@0: Erin is round.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "round" "+")
@0: Dave is white.[(triple1)] Erin is green.[(triple2)] Erin is kind.[(triple3)] @1: Erin is cold.[(((triple2 triple3) -> rule4))] @2: Erin is white.[(((((triple2 triple3) -> rule4)) -> rule5))]
Dave is white.
("Dave" "is" "white" "+")
triple1
Erin is green.
("Erin" "is" "green" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is cold.
("Erin" "is" "cold" "+")
((triple2 triple3) -> (rule4 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((((triple2 triple3) -> (rule4 % int2))) -> (rule5 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is cold.
("Erin" "is" "cold" "+")
int2