Dave is not rough. Gary is kind. Harry is round. All kind things are blue. If Gary is blue then Gary is not nice. If something is nice then it is kind. White things are cold. If Gary is kind and Gary is not nice then Gary is white. All nice, cold things are round.
Dave is not rough.
("Dave" "is" "rough" "-")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
All kind things are blue.
((("something" "is" "kind" "+")) -> ("something" "is" "blue" "+"))
If Gary is blue then Gary is not nice.
((("Gary" "is" "blue" "+")) -> ("Gary" "is" "nice" "-"))
If something is nice then it is kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
White things are cold.
((("something" "is" "white" "+")) -> ("something" "is" "cold" "+"))
If Gary is kind and Gary is not nice then Gary is white.
((("Gary" "is" "kind" "+") ("Gary" "is" "nice" "~")) -> ("Gary" "is" "white" "+"))
All nice, cold things are round.
((("something" "is" "nice" "+") ("something" "is" "cold" "+")) -> ("something" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple3)]
("Harry" "is" "round" "+")
triple3
Gary is not kind.
False
1
inv-proof
[(triple2)]
("Gary" "is" "kind" "-")
triple2
Gary is blue.
True
2
proof
[(((triple2) -> rule1))]
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not blue.
False
2
inv-proof
[(((triple2) -> rule1))]
("Gary" "is" "blue" "-")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not nice.
True
3
proof
[(((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "nice" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is nice.
False
3
inv-proof
[(((((triple2) -> rule1)) -> rule2))]
("Gary" "is" "nice" "+")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
True
5
proof
[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "white" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is not white.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule5))]
("Gary" "is" "white" "-")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Dave is not cold.
Unknown
inv-rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "cold" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "cold" "-")
Gary is round.
Unknown
rconc
[@1: Gary is round.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "round" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Gary is rough.
Unknown
random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "+")
@0: Dave is not rough.[(triple1)] Gary is kind.[(triple2)] Harry is round.[(triple3)] @1: Gary is blue.[(((triple2) -> rule1))] @2: Gary is not nice.[(((((triple2) -> rule1)) -> rule2))] @3: Gary is white.[(((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule5))] @4: Gary is cold.[(((((triple2 ((((triple2) -> rule1)) -> rule2)) -> rule5)) -> rule4))]
Dave is not rough.
("Dave" "is" "rough" "-")
triple1
Gary is kind.
("Gary" "is" "kind" "+")
triple2
Harry is round.
("Harry" "is" "round" "+")
triple3
Gary is blue.
("Gary" "is" "blue" "+")
((triple2) -> (rule1 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
((((triple2) -> (rule1 % int2))) -> (rule2 % int1))
Gary is not nice.
("Gary" "is" "nice" "-")
int1
Gary is blue.
("Gary" "is" "blue" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((triple2 ((((triple2) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is not nice.
("Gary" "is" "nice" "-")
int2
Gary is blue.
("Gary" "is" "blue" "+")
int3
Gary is cold.
("Gary" "is" "cold" "+")
((((triple2 ((((triple2) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is not nice.
("Gary" "is" "nice" "-")
int3
Gary is blue.
("Gary" "is" "blue" "+")
int4