Charlie is big. Dave is not quiet. Gary is kind. Harry is round. All blue, kind things are not cold. All round things are not cold. If Gary is blue and Gary is quiet then Gary is kind. If something is white then it is quiet. Cold things are big. All big things are white.
Charlie is big.
("Charlie" "is" "big" "+")
Dave is not quiet.
("Dave" "is" "quiet" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
All blue, kind things are not cold.
((("something" "is" "blue" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "-"))
All round things are not cold.
((("something" "is" "round" "+")) -> ("something" "is" "cold" "-"))
If Gary is blue and Gary is quiet then Gary is kind.
((("Gary" "is" "blue" "+") ("Gary" "is" "quiet" "+")) -> ("Gary" "is" "kind" "+"))
If something is white then it is quiet.
((("something" "is" "white" "+")) -> ("something" "is" "quiet" "+"))
Cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
All big things are white.
((("something" "is" "big" "+")) -> ("something" "is" "white" "+"))
Charlie is big.
True
1
proof
[(triple1)]
("Charlie" "is" "big" "+")
triple1
Harry is not round.
False
1
inv-proof
[(triple4)]
("Harry" "is" "round" "-")
triple4
Harry is not cold.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Harry is cold.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "cold" "+")
((triple4) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Charlie is quiet.
True
3
proof
[(((((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not quiet.
False
3
inv-proof
[(((((triple1) -> rule6)) -> rule4))]
("Charlie" "is" "quiet" "-")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@2: Dave is white.[CWA. Example of deepest failure = (rule6 <- rule5 <- FAIL)]]
("Dave" "is" "white" "-")
Harry is big.
Unknown
rconc
[@1: Harry is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "big" "+")
Gary is not quiet.
Unknown
inv-rconc
[@3: Gary is quiet.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule5 <- FAIL)]]
("Gary" "is" "quiet" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
Dave is not blue.
Unknown
inv-random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Charlie is big.[(triple1)] Dave is not quiet.[(triple2)] Gary is kind.[(triple3)] Harry is round.[(triple4)] @1: Charlie is white.[(((triple1) -> rule6))] Harry is not cold.[(((triple4) -> rule2))] @2: Charlie is quiet.[(((((triple1) -> rule6)) -> rule4))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Dave is not quiet.
("Dave" "is" "quiet" "-")
triple2
Gary is kind.
("Gary" "is" "kind" "+")
triple3
Harry is round.
("Harry" "is" "round" "+")
triple4
Charlie is white.
("Charlie" "is" "white" "+")
((triple1) -> (rule6 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Harry is not cold.
("Harry" "is" "cold" "-")
((triple4) -> (rule2 % int1))
Harry is not cold.
("Harry" "is" "cold" "-")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2