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