Bob is smart. Bob is not white. Dave is kind. Dave is nice. Dave is rough. Harry is furry. Harry is green. Harry is nice. Harry is rough. Harry is smart. If Bob is green then Bob is rough. If something is white then it is kind. All smart things are green. If something is smart and green then it is rough. If something is smart then it is not white. Kind, green things are smart.
Bob is smart.
("Bob" "is" "smart" "+")
Bob is not white.
("Bob" "is" "white" "-")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If Bob is green then Bob is rough.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "rough" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
All smart things are green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
If something is smart and green then it is rough.
((("something" "is" "smart" "+") ("something" "is" "green" "+")) -> ("something" "is" "rough" "+"))
If something is smart then it is not white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
Kind, green things are smart.
((("something" "is" "kind" "+") ("something" "is" "green" "+")) -> ("something" "is" "smart" "+"))
Harry is rough.
True
1
proof
[(triple9 OR ((triple10 triple7) -> rule4) OR ((triple10 ((triple10) -> rule3)) -> rule4))]
("Harry" "is" "rough" "+")
triple9
((triple10 triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Dave is not kind.
False
1
inv-proof
[(triple3)]
("Dave" "is" "kind" "-")
triple3
Harry is not white.
True
2
proof
[(((triple10) -> rule5))]
("Harry" "is" "white" "-")
((triple10) -> (rule5 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule3))]
("Bob" "is" "green" "-")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
True
3
proof
[(((((triple1) -> rule3)) -> rule1) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
("Bob" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not rough.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
("Bob" "is" "rough" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule3 <- rule6 <- FAIL)]]
("Dave" "is" "green" "-")
Bob is kind.
Unknown
rconc
[@1: Bob is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "kind" "+")
Harry is not kind.
Unknown
inv-rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "kind" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Bob is furry.
Unknown
random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is not white.[(triple2 OR ((triple1) -> rule5))] Bob is smart.[(triple1)] Dave is kind.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5)] Harry is furry.[(triple6)] Harry is green.[(triple7 OR ((triple10) -> rule3))] Harry is nice.[(triple8)] Harry is rough.[(triple9 OR ((triple10 triple7) -> rule4) OR ((triple10 ((triple10) -> rule3)) -> rule4))] Harry is smart.[(triple10)] @1: Bob is green.[(((triple1) -> rule3))] Harry is not white.[(((triple10) -> rule5))] @2: Bob is rough.[(((((triple1) -> rule3)) -> rule1) OR ((triple1 ((triple1) -> rule3)) -> rule4))]
Bob is not white.
("Bob" "is" "white" "-")
triple2
((triple1) -> (rule5 % int1))
Bob is not white.
("Bob" "is" "white" "-")
int1
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
Harry is furry.
("Harry" "is" "furry" "+")
triple6
Harry is green.
("Harry" "is" "green" "+")
triple7
((triple10) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
((triple10 triple7) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((triple10 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple10
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((triple10) -> (rule5 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((triple1 ((triple1) -> (rule3 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2