Bob is big. Bob is cold. Bob is kind. Bob is quiet. Bob is round. Charlie is big. Charlie is blue. Charlie is cold. Charlie is green. Charlie is kind. Charlie is round. Dave is blue. Dave is quiet. Harry is green. Harry is quiet. Harry is round. Cold things are kind.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
Cold things are kind.
((("something" "is" "cold" "+")) -> ("something" "is" "kind" "+"))
Bob is quiet.
True
1
proof
[(triple4)]
("Bob" "is" "quiet" "+")
triple4
Bob is not kind.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule1))]
("Bob" "is" "kind" "-")
triple3
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "kind" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is kind.[(triple3 OR ((triple2) -> rule1))] Bob is quiet.[(triple4)] Bob is round.[(triple5)] Charlie is big.[(triple6)] Charlie is blue.[(triple7)] Charlie is cold.[(triple8)] Charlie is green.[(triple9)] Charlie is kind.[(triple10 OR ((triple8) -> rule1))] Charlie is round.[(triple11)] Dave is blue.[(triple12)] Dave is quiet.[(triple13)] Harry is green.[(triple14)] Harry is quiet.[(triple15)] Harry is round.[(triple16)]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
((triple2) -> (rule1 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is blue.
("Charlie" "is" "blue" "+")
triple7
Charlie is cold.
("Charlie" "is" "cold" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
((triple8) -> (rule1 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
triple11
Dave is blue.
("Dave" "is" "blue" "+")
triple12
Dave is quiet.
("Dave" "is" "quiet" "+")
triple13
Harry is green.
("Harry" "is" "green" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is round.
("Harry" "is" "round" "+")
triple16