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