Anne is blue. Anne is kind. Anne is young. Bob is quiet. Bob is smart. Bob is young. Harry is blue. Harry is green. Harry is kind. Harry is quiet. Harry is rough. Harry is smart. Quiet, blue things are young. All green things are blue.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Bob is young.
("Bob" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet, blue things are young.
((("something" "is" "quiet" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
All green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Bob is young.
True
1
proof
[(triple6)]
("Bob" "is" "young" "+")
triple6
Harry is not smart.
False
1
inv-proof
[(triple12)]
("Harry" "is" "smart" "-")
triple12
Harry is young.
True
3
proof
[(((triple10 triple7) -> rule1) OR ((triple10 ((triple8) -> rule2)) -> rule1))]
("Harry" "is" "young" "+")
((triple10 triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not young.
False
3
inv-proof
[(((triple10 triple7) -> rule1) OR ((triple10 ((triple8) -> rule2)) -> rule1))]
("Harry" "is" "young" "-")
((triple10 triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not green.
Unknown
inv-random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is blue.[(triple1)] Anne is kind.[(triple2)] Anne is young.[(triple3)] Bob is quiet.[(triple4)] Bob is smart.[(triple5)] Bob is young.[(triple6)] Harry is blue.[(triple7 OR ((triple8) -> rule2))] Harry is green.[(triple8)] Harry is kind.[(triple9)] Harry is quiet.[(triple10)] Harry is rough.[(triple11)] Harry is smart.[(triple12)] @1: Harry is young.[(((triple10 triple7) -> rule1) OR ((triple10 ((triple8) -> rule2)) -> rule1))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple4
Bob is smart.
("Bob" "is" "smart" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
((triple8) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple8
Harry is kind.
("Harry" "is" "kind" "+")
triple9
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Harry is smart.
("Harry" "is" "smart" "+")
triple12
Harry is young.
("Harry" "is" "young" "+")
((triple10 triple7) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((triple10 ((triple8) -> (rule2 % int2))) -> (rule1 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2