Charlie is blue. Charlie is kind. Dave is kind. Dave is rough. Erin is big. Erin is not kind. Erin is rough. If something is cold and kind then it is rough. If something is nice then it is cold. All blue things are nice.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is not kind.
("Erin" "is" "kind" "-")
Erin is rough.
("Erin" "is" "rough" "+")
If something is cold and kind then it is rough.
((("something" "is" "cold" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
If something is nice then it is cold.
((("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Erin is not kind.
True
1
proof
[(triple6)]
("Erin" "is" "kind" "-")
triple6
Erin is kind.
False
1
inv-proof
[(triple6)]
("Erin" "is" "kind" "+")
triple6
Charlie is nice.
True
2
proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is not nice.
False
2
inv-proof
[(((triple1) -> rule3))]
("Charlie" "is" "nice" "-")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
True
3
proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is not cold.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Erin is not nice.
Unknown
inv-rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "nice" "-")
Dave is cold.
Unknown
rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Dave" "is" "cold" "+")
Erin is not cold.
Unknown
inv-rconc
[@2: Erin is cold.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Erin" "is" "cold" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Erin is not blue.
Unknown
inv-random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
@0: Charlie is blue.[(triple1)] Charlie is kind.[(triple2)] Dave is kind.[(triple3)] Dave is rough.[(triple4)] Erin is big.[(triple5)] Erin is not kind.[(triple6)] Erin is rough.[(triple7)] @1: Charlie is nice.[(((triple1) -> rule3))] @2: Charlie is cold.[(((((triple1) -> rule3)) -> rule2))] @3: Charlie is rough.[(((((((triple1) -> rule3)) -> rule2) triple2) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Erin is big.
("Erin" "is" "big" "+")
triple5
Erin is not kind.
("Erin" "is" "kind" "-")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule3 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
((((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
((((((triple1) -> (rule3 % int3))) -> (rule2 % int2)) triple2) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3