Bob is blue. Bob is kind. Bob is not round. Bob is young. Dave is blue. Dave is rough. Dave is round. Dave is white. Dave is young. Harry is kind. Harry is nice. Harry is not rough. Harry is round. Harry is white. Harry is young. If Dave is not blue then Dave is kind. If something is round then it is young. Young things are nice. If something is round and blue then it is nice. If Harry is kind then Harry is round. All rough things are round. If something is blue and not white then it is rough. If Dave is rough and Dave is not young then Dave is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not round.
("Bob" "is" "round" "-")
Bob is young.
("Bob" "is" "young" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is not rough.
("Harry" "is" "rough" "-")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Dave is not blue then Dave is kind.
((("Dave" "is" "blue" "~")) -> ("Dave" "is" "kind" "+"))
If something is round then it is young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "+"))
Young things are nice.
((("something" "is" "young" "+")) -> ("something" "is" "nice" "+"))
If something is round and blue then it is nice.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
If Harry is kind then Harry is round.
((("Harry" "is" "kind" "+")) -> ("Harry" "is" "round" "+"))
All rough things are round.
((("something" "is" "rough" "+")) -> ("something" "is" "round" "+"))
If something is blue and not white then it is rough.
((("something" "is" "blue" "+") ("something" "is" "white" "~")) -> ("something" "is" "rough" "+"))
If Dave is rough and Dave is not young then Dave is nice.
((("Dave" "is" "rough" "+") ("Dave" "is" "young" "~")) -> ("Dave" "is" "nice" "+"))
Harry is young.
True
1
proof
[(triple15 OR ((triple13) -> rule2) OR ((((triple10) -> rule5)) -> rule2))]
("Harry" "is" "young" "+")
triple15
((triple13) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not kind.
False
1
inv-proof
[(triple10)]
("Harry" "is" "kind" "-")
triple10
Bob is nice.
True
2
proof
[(((triple4) -> rule3))]
("Bob" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple9) -> rule3) OR ((triple7 triple5) -> rule4) OR ((((triple7) -> rule2)) -> rule3) OR ((((triple6) -> rule6) triple5) -> rule4) OR ((((((triple6) -> rule6)) -> rule2)) -> rule3))]
("Dave" "is" "nice" "-")
((triple9) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple6) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "rough" "-")
Dave is kind.
Unknown
rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "kind" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Bob is blue.[(triple1)] Bob is kind.[(triple2)] Bob is not round.[(triple3)] Bob is young.[(triple4)] Dave is blue.[(triple5)] Dave is rough.[(triple6)] Dave is round.[(triple7 OR ((triple6) -> rule6))] Dave is white.[(triple8)] Dave is young.[(triple9 OR ((triple7) -> rule2) OR ((((triple6) -> rule6)) -> rule2))] Harry is kind.[(triple10)] Harry is nice.[(triple11 OR ((triple15) -> rule3) OR ((((triple13) -> rule2)) -> rule3) OR ((((((triple10) -> rule5)) -> rule2)) -> rule3))] Harry is not rough.[(triple12)] Harry is round.[(triple13 OR ((triple10) -> rule5))] Harry is white.[(triple14)] Harry is young.[(triple15 OR ((triple13) -> rule2) OR ((((triple10) -> rule5)) -> rule2))] @1: Bob is nice.[(((triple4) -> rule3))] Dave is nice.[(((triple9) -> rule3) OR ((triple7 triple5) -> rule4) OR ((((triple7) -> rule2)) -> rule3) OR ((((triple6) -> rule6) triple5) -> rule4) OR ((((((triple6) -> rule6)) -> rule2)) -> rule3))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Bob is not round.
("Bob" "is" "round" "-")
triple3
Bob is young.
("Bob" "is" "young" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is rough.
("Dave" "is" "rough" "+")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple7
((triple6) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
triple8
Dave is young.
("Dave" "is" "young" "+")
triple9
((triple7) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple6) -> (rule6 % int2))) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple10
Harry is nice.
("Harry" "is" "nice" "+")
triple11
((triple15) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple13) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not rough.
("Harry" "is" "rough" "-")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
((triple10) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
((triple13) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
((triple4) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple9) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((triple7 triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
((((triple7) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((((triple6) -> (rule6 % int2)) triple5) -> (rule4 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
((((((triple6) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3