Anne is nice. Anne is quiet. Anne is rough. Anne is white. Bob is cold. Bob is green. Bob is nice. Harry is blue. Harry is cold. Harry is green. Harry is quiet. Harry is white. Green people are nice. If someone is rough and blue then they are green. Nice people are rough.
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Green people are nice.
((("someone" "is" "green" "+")) -> ("someone" "is" "nice" "+"))
If someone is rough and blue then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "green" "+"))
Nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
Bob is cold.
True
1
proof
[(triple5)]
("Bob" "is" "cold" "+")
triple5
Anne is not nice.
False
1
inv-proof
[(triple1)]
("Anne" "is" "nice" "-")
triple1
Bob is rough.
True
2
proof
[(((triple7) -> rule3) OR ((((triple6) -> rule1)) -> rule3))]
("Bob" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is not nice.
False
2
inv-proof
[(((triple10) -> rule1))]
("Harry" "is" "nice" "-")
((triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Anne is not green.
Unknown
inv-rconc
[@1: Anne is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "green" "-")
Anne is cold.
Unknown
random
[@0: Anne is cold.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "cold" "+")
Anne is not blue.
Unknown
inv-random
[@0: Anne is blue.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "blue" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Anne is nice.[(triple1)] Anne is quiet.[(triple2)] Anne is rough.[(triple3 OR ((triple1) -> rule3))] Anne is white.[(triple4)] Bob is cold.[(triple5)] Bob is green.[(triple6)] Bob is nice.[(triple7 OR ((triple6) -> rule1))] Harry is blue.[(triple8)] Harry is cold.[(triple9)] Harry is green.[(triple10)] Harry is quiet.[(triple11)] Harry is white.[(triple12)] @1: Bob is rough.[(((triple7) -> rule3) OR ((((triple6) -> rule1)) -> rule3))] Harry is nice.[(((triple10) -> rule1))] @2: Harry is rough.[(((((triple10) -> rule1)) -> rule3))]
Anne is nice.
("Anne" "is" "nice" "+")
triple1
Anne is quiet.
("Anne" "is" "quiet" "+")
triple2
Anne is rough.
("Anne" "is" "rough" "+")
triple3
((triple1) -> (rule3 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is white.
("Anne" "is" "white" "+")
triple4
Bob is cold.
("Bob" "is" "cold" "+")
triple5
Bob is green.
("Bob" "is" "green" "+")
triple6
Bob is nice.
("Bob" "is" "nice" "+")
triple7
((triple6) -> (rule1 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is green.
("Harry" "is" "green" "+")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple7) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple6) -> (rule1 % int2))) -> (rule3 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((triple10) -> (rule1 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple10) -> (rule1 % int2))) -> (rule3 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2