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