Erin is nice. Fiona is rough. Gary is nice. Harry is quiet. If Gary is nice then Gary is white. If something is white then it is kind. Kind things are quiet.
Erin is nice.
("Erin" "is" "nice" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Gary is nice then Gary is white.
((("Gary" "is" "nice" "+")) -> ("Gary" "is" "white" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
Kind things are quiet.
((("something" "is" "kind" "+")) -> ("something" "is" "quiet" "+"))
Gary is nice.
True
1
proof
[(triple3)]
("Gary" "is" "nice" "+")
triple3
Gary is not nice.
False
1
inv-proof
[(triple3)]
("Gary" "is" "nice" "-")
triple3
Gary is white.
True
2
proof
[(((triple3) -> rule1))]
("Gary" "is" "white" "+")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not white.
False
2
inv-proof
[(((triple3) -> rule1))]
("Gary" "is" "white" "-")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
True
3
proof
[(((((triple3) -> rule1)) -> rule2))]
("Gary" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not kind.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Gary" "is" "kind" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
True
4
proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is not quiet.
False
4
inv-proof
[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Erin is not kind.
Unknown
inv-rconc
[@1: Erin is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "kind" "-")
Fiona is kind.
Unknown
rconc
[@1: Fiona is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not quiet.
Unknown
inv-rconc
[@2: Fiona is quiet.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "quiet" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "+")
Harry is not big.
Unknown
inv-random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Erin is white.
Unknown
random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "+")
@0: Erin is nice.[(triple1)] Fiona is rough.[(triple2)] Gary is nice.[(triple3)] Harry is quiet.[(triple4)] @1: Gary is white.[(((triple3) -> rule1))] @2: Gary is kind.[(((((triple3) -> rule1)) -> rule2))] @3: Gary is quiet.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
Erin is nice.
("Erin" "is" "nice" "+")
triple1
Fiona is rough.
("Fiona" "is" "rough" "+")
triple2
Gary is nice.
("Gary" "is" "nice" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Gary is white.
("Gary" "is" "white" "+")
((triple3) -> (rule1 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is quiet.
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3