Dave is big. Dave is cold. Dave is rough. Dave is round. Gary is red. Harry is big. Harry is rough. If Gary is not red then Gary is not kind. If someone is round then they are cold. Red people are kind. All kind people are young. If Harry is not cold then Harry is kind. If Gary is young and Gary is red then Gary is cold.
Dave is big.
("Dave" "is" "big" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Gary is red.
("Gary" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Gary is not red then Gary is not kind.
((("Gary" "is" "red" "~")) -> ("Gary" "is" "kind" "-"))
If someone is round then they are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
Red people are kind.
((("someone" "is" "red" "+")) -> ("someone" "is" "kind" "+"))
All kind people are young.
((("someone" "is" "kind" "+")) -> ("someone" "is" "young" "+"))
If Harry is not cold then Harry is kind.
((("Harry" "is" "cold" "~")) -> ("Harry" "is" "kind" "+"))
If Gary is young and Gary is red then Gary is cold.
((("Gary" "is" "young" "+") ("Gary" "is" "red" "+")) -> ("Gary" "is" "cold" "+"))
Dave is big.
True
1
proof
[(triple1)]
("Dave" "is" "big" "+")
triple1
Dave is not cold.
False
1
inv-proof
[(triple2 OR ((triple4) -> rule2))]
("Dave" "is" "cold" "-")
triple2
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Gary is kind.
True
2
proof
[(((triple5) -> rule3))]
("Gary" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is not kind.
False
2
inv-proof
[(((triple5) -> rule3))]
("Gary" "is" "kind" "-")
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
True
3
proof
[(((((triple5) -> rule3)) -> rule4))]
("Gary" "is" "young" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is not young.
False
3
inv-proof
[(((((triple5) -> rule3)) -> rule4))]
("Gary" "is" "young" "-")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
True
5
proof
[(((((((triple5) -> rule3)) -> rule4) triple5) -> rule6))]
("Gary" "is" "cold" "+")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Gary is not cold.
False
5
inv-proof
[(((((((triple5) -> rule3)) -> rule4) triple5) -> rule6))]
("Gary" "is" "cold" "-")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "kind" "+")
Harry is not young.
Unknown
inv-rconc
[@2: Harry is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Harry" "is" "young" "-")
Dave is young.
Unknown
rconc
[@2: Dave is young.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Dave" "is" "young" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Gary is big.
Unknown
random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "+")
@0: Dave is big.[(triple1)] Dave is cold.[(triple2 OR ((triple4) -> rule2))] Dave is rough.[(triple3)] Dave is round.[(triple4)] Gary is red.[(triple5)] Harry is big.[(triple6)] Harry is rough.[(triple7)] @1: Gary is kind.[(((triple5) -> rule3))] @2: Gary is young.[(((((triple5) -> rule3)) -> rule4))] @3: Gary is cold.[(((((((triple5) -> rule3)) -> rule4) triple5) -> rule6))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
((triple4) -> (rule2 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple3
Dave is round.
("Dave" "is" "round" "+")
triple4
Gary is red.
("Gary" "is" "red" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Gary is kind.
("Gary" "is" "kind" "+")
((triple5) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
((((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is kind.
("Gary" "is" "kind" "+")
int2
Gary is cold.
("Gary" "is" "cold" "+")
((((((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule6 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
int3