Charlie is kind. Dave is cold. Dave is green. Dave is nice. Dave is round. Erin is kind. Erin is round. Harry is big. Harry is green. Harry is kind. If something is big and round then it is green. Cold, quiet things are kind. If something is quiet and kind then it is cold. If Dave is quiet then Dave is cold. Cold things are kind. Big things are green. If Charlie is quiet then Charlie is big. All nice things are kind.
Charlie is kind.
("Charlie" "is" "kind" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
If something is big and round then it is green.
((("something" "is" "big" "+") ("something" "is" "round" "+")) -> ("something" "is" "green" "+"))
Cold, quiet things are kind.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
If something is quiet and kind then it is cold.
((("something" "is" "quiet" "+") ("something" "is" "kind" "+")) -> ("something" "is" "cold" "+"))
If Dave is quiet then Dave is cold.
((("Dave" "is" "quiet" "+")) -> ("Dave" "is" "cold" "+"))
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Big things are green.
((("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Charlie is quiet then Charlie is big.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "big" "+"))
All nice things are kind.
((("something" "is" "nice" "+")) -> ("something" "is" "kind" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Dave is not cold.
False
1
inv-proof
[(triple2)]
("Dave" "is" "cold" "-")
triple2
Dave is kind.
True
2
proof
[(((triple2) -> rule5) OR ((triple4) -> rule8))]
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple4) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is not kind.
False
2
inv-proof
[(((triple2) -> rule5) OR ((triple4) -> rule8))]
("Dave" "is" "kind" "-")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple4) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Charlie is not green.
Unknown
inv-rconc
[@2: Charlie is green.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Charlie" "is" "big" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Harry is quiet.
Unknown
random
[@0: Harry is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "quiet" "+")
@0: Charlie is kind.[(triple1)] Dave is cold.[(triple2)] Dave is green.[(triple3)] Dave is nice.[(triple4)] Dave is round.[(triple5)] Erin is kind.[(triple6)] Erin is round.[(triple7)] Harry is big.[(triple8)] Harry is green.[(triple9 OR ((triple8) -> rule6))] Harry is kind.[(triple10)] @1: Dave is kind.[(((triple2) -> rule5) OR ((triple4) -> rule8))]
Charlie is kind.
("Charlie" "is" "kind" "+")
triple1
Dave is cold.
("Dave" "is" "cold" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is round.
("Dave" "is" "round" "+")
triple5
Erin is kind.
("Erin" "is" "kind" "+")
triple6
Erin is round.
("Erin" "is" "round" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is green.
("Harry" "is" "green" "+")
triple9
((triple8) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Dave is kind.
("Dave" "is" "kind" "+")
((triple2) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((triple4) -> (rule8 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1