Bob is nice. Erin is quiet. If Erin is quiet and Erin is nice then Erin is white. All big people are nice. If someone is quiet then they are nice. Big, nice people are quiet. If someone is rough and blue then they are cold. Big people are cold.
Bob is nice.
("Bob" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
If Erin is quiet and Erin is nice then Erin is white.
((("Erin" "is" "quiet" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "white" "+"))
All big people are nice.
((("someone" "is" "big" "+")) -> ("someone" "is" "nice" "+"))
If someone is quiet then they are nice.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "nice" "+"))
Big, nice people are quiet.
((("someone" "is" "big" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
If someone is rough and blue then they are cold.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "cold" "+"))
Big people are cold.
((("someone" "is" "big" "+")) -> ("someone" "is" "cold" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple2)]
("Erin" "is" "quiet" "-")
triple2
Erin is nice.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is not nice.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "nice" "-")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
True
4
proof
[(((triple2 ((triple2) -> rule3)) -> rule1))]
("Erin" "is" "white" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not white.
False
4
inv-proof
[(((triple2 ((triple2) -> rule3)) -> rule1))]
("Erin" "is" "white" "-")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "quiet" "+")
Bob is not cold.
Unknown
inv-rconc
[@1: Bob is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "cold" "-")
Erin is rough.
Unknown
random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "+")
Bob is not rough.
Unknown
inv-random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is nice.[(triple1)] Erin is quiet.[(triple2)] @1: Erin is nice.[(((triple2) -> rule3))] @2: Erin is white.[(((triple2 ((triple2) -> rule3)) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple2 ((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2