Bob is green. Bob is red. Bob is round. Bob is not smart. Bob is not young. Charlie is furry. Charlie is young. Dave is green. Dave is not round. Dave is smart. Harry is furry. Harry is red. Harry is round. Harry is smart. Harry is young. All young, smart things are green. Green, smart things are not white. White, red things are not round.
Bob is green.
("Bob" "is" "green" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is not smart.
("Bob" "is" "smart" "-")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is green.
("Dave" "is" "green" "+")
Dave is not round.
("Dave" "is" "round" "-")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All young, smart things are green.
((("something" "is" "young" "+") ("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Green, smart things are not white.
((("something" "is" "green" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "-"))
White, red things are not round.
((("something" "is" "white" "+") ("something" "is" "red" "+")) -> ("something" "is" "round" "-"))
Harry is smart.
True
1
proof
[(triple14)]
("Harry" "is" "smart" "+")
triple14
Harry is not smart.
False
1
inv-proof
[(triple14)]
("Harry" "is" "smart" "-")
triple14
Harry is green.
True
3
proof
[(((triple15 triple14) -> rule1))]
("Harry" "is" "green" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Dave is white.
False
3
inv-proof
[(((triple8 triple10) -> rule2))]
("Dave" "is" "white" "+")
((triple8 triple10) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Harry is not white.
True
5
proof
[(((((triple15 triple14) -> rule1) triple14) -> rule2))]
("Harry" "is" "white" "-")
((((triple15 triple14) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
False
5
inv-proof
[(((((triple15 triple14) -> rule1) triple14) -> rule2))]
("Harry" "is" "white" "+")
((((triple15 triple14) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Charlie is not green.
Unknown
inv-rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Charlie is not smart.
Unknown
inv-random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Dave is not furry.
Unknown
inv-random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
@0: Bob is green.[(triple1)] Bob is not smart.[(triple4)] Bob is not young.[(triple5)] Bob is red.[(triple2)] Bob is round.[(triple3)] Charlie is furry.[(triple6)] Charlie is young.[(triple7)] Dave is green.[(triple8)] Dave is not round.[(triple9)] Dave is smart.[(triple10)] Harry is furry.[(triple11)] Harry is red.[(triple12)] Harry is round.[(triple13)] Harry is smart.[(triple14)] Harry is young.[(triple15)] @1: Dave is not white.[(((triple8 triple10) -> rule2))] Harry is green.[(((triple15 triple14) -> rule1))] @2: Harry is not white.[(((((triple15 triple14) -> rule1) triple14) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not smart.
("Bob" "is" "smart" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple2
Bob is round.
("Bob" "is" "round" "+")
triple3
Charlie is furry.
("Charlie" "is" "furry" "+")
triple6
Charlie is young.
("Charlie" "is" "young" "+")
triple7
Dave is green.
("Dave" "is" "green" "+")
triple8
Dave is not round.
("Dave" "is" "round" "-")
triple9
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Harry is round.
("Harry" "is" "round" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Dave is not white.
("Dave" "is" "white" "-")
((triple8 triple10) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple15 triple14) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not white.
("Harry" "is" "white" "-")
((((triple15 triple14) -> (rule1 % int2)) triple14) -> (rule2 % int1))
Harry is not white.
("Harry" "is" "white" "-")
int1
Harry is green.
("Harry" "is" "green" "+")
int2