Anne is big. Anne is blue. Anne is nice. Anne is not quiet. Bob is big. Bob is not blue. Bob is kind. Bob is quiet. Bob is rough. Charlie is big. Charlie is nice. Charlie is quiet. Charlie is rough. Harry is big. Harry is blue. Harry is kind. Kind, nice things are rough. If something is blue and not cold then it is rough. All blue things are nice.
Anne is big.
("Anne" "is" "big" "+")
Anne is blue.
("Anne" "is" "blue" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is not quiet.
("Anne" "is" "quiet" "-")
Bob is big.
("Bob" "is" "big" "+")
Bob is not blue.
("Bob" "is" "blue" "-")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Kind, nice things are rough.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If something is blue and not cold then it is rough.
((("something" "is" "blue" "+") ("something" "is" "cold" "~")) -> ("something" "is" "rough" "+"))
All blue things are nice.
((("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Harry is blue.
True
1
proof
[(triple15)]
("Harry" "is" "blue" "+")
triple15
Harry is not big.
False
1
inv-proof
[(triple14)]
("Harry" "is" "big" "-")
triple14
Harry is nice.
True
2
proof
[(((triple15) -> rule3))]
("Harry" "is" "nice" "+")
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is not nice.
False
2
inv-proof
[(((triple15) -> rule3))]
("Harry" "is" "nice" "-")
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
True
4
proof
[(((triple16 ((triple15) -> rule3)) -> rule1))]
("Harry" "is" "rough" "+")
((triple16 ((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((triple16 ((triple15) -> rule3)) -> rule1))]
("Harry" "is" "rough" "-")
((triple16 ((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Anne is not rough.
Unknown
inv-rconc
[@1: Anne is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Anne" "is" "rough" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Charlie is not cold.
Unknown
inv-random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is blue.[(triple2)] Anne is nice.[(triple3 OR ((triple2) -> rule3))] Anne is not quiet.[(triple4)] Bob is big.[(triple5)] Bob is kind.[(triple7)] Bob is not blue.[(triple6)] Bob is quiet.[(triple8)] Bob is rough.[(triple9)] Charlie is big.[(triple10)] Charlie is nice.[(triple11)] Charlie is quiet.[(triple12)] Charlie is rough.[(triple13)] Harry is big.[(triple14)] Harry is blue.[(triple15)] Harry is kind.[(triple16)] @1: Harry is nice.[(((triple15) -> rule3))] @2: Harry is rough.[(((triple16 ((triple15) -> rule3)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is blue.
("Anne" "is" "blue" "+")
triple2
Anne is nice.
("Anne" "is" "nice" "+")
triple3
((triple2) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is not quiet.
("Anne" "is" "quiet" "-")
triple4
Bob is big.
("Bob" "is" "big" "+")
triple5
Bob is kind.
("Bob" "is" "kind" "+")
triple7
Bob is not blue.
("Bob" "is" "blue" "-")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
triple8
Bob is rough.
("Bob" "is" "rough" "+")
triple9
Charlie is big.
("Charlie" "is" "big" "+")
triple10
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple12
Charlie is rough.
("Charlie" "is" "rough" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is blue.
("Harry" "is" "blue" "+")
triple15
Harry is kind.
("Harry" "is" "kind" "+")
triple16
Harry is nice.
("Harry" "is" "nice" "+")
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple16 ((triple15) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2