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