Anne is big. Anne is not nice. Anne is red. Anne is rough. Dave is big. Dave is rough. Harry is cold. Harry is nice. Harry is red. Harry is young. Red things are green. All nice things are not rough. If something is cold and nice then it is young.
Anne is big.
("Anne" "is" "big" "+")
Anne is not nice.
("Anne" "is" "nice" "-")
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Dave is big.
("Dave" "is" "big" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is young.
("Harry" "is" "young" "+")
Red things are green.
((("something" "is" "red" "+")) -> ("something" "is" "green" "+"))
All nice things are not rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "-"))
If something is cold and nice then it is young.
((("something" "is" "cold" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Harry is red.
True
1
proof
[(triple9)]
("Harry" "is" "red" "+")
triple9
Dave is not rough.
False
1
inv-proof
[(triple6)]
("Dave" "is" "rough" "-")
triple6
Harry is not rough.
True
2
proof
[(((triple8) -> rule2))]
("Harry" "is" "rough" "-")
((triple8) -> (rule2 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1
Anne is not green.
False
2
inv-proof
[(((triple3) -> rule1))]
("Anne" "is" "green" "-")
((triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Anne is young.
Unknown
rconc
[@1: Anne is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Anne" "is" "young" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Anne is big.[(triple1)] Anne is not nice.[(triple2)] Anne is red.[(triple3)] Anne is rough.[(triple4)] Dave is big.[(triple5)] Dave is rough.[(triple6)] Harry is cold.[(triple7)] Harry is nice.[(triple8)] Harry is red.[(triple9)] Harry is young.[(triple10 OR ((triple7 triple8) -> rule3))] @1: Anne is green.[(((triple3) -> rule1))] Harry is green.[(((triple9) -> rule1))] Harry is not rough.[(((triple8) -> rule2))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is not nice.
("Anne" "is" "nice" "-")
triple2
Anne is red.
("Anne" "is" "red" "+")
triple3
Anne is rough.
("Anne" "is" "rough" "+")
triple4
Dave is big.
("Dave" "is" "big" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is red.
("Harry" "is" "red" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
((triple7 triple8) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is green.
("Anne" "is" "green" "+")
((triple3) -> (rule1 % int1))
Anne is green.
("Anne" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple9) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not rough.
("Harry" "is" "rough" "-")
((triple8) -> (rule2 % int1))
Harry is not rough.
("Harry" "is" "rough" "-")
int1