Bob is nice. Bob is round. Charlie is quiet. Harry is kind. Harry is nice. Harry is quiet. Harry is round. If something is round and quiet then it is green. If something is green and nice then it is blue. All green, round things are blue. Green things are blue. Smart, blue things are not nice. If Bob is kind and Bob is smart then Bob is green. If Harry is kind and Harry is blue then Harry is not smart. If Bob is smart and Bob is blue then Bob is round.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is round.
("Harry" "is" "round" "+")
If something is round and quiet then it is green.
((("something" "is" "round" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is green and nice then it is blue.
((("something" "is" "green" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
All green, round things are blue.
((("something" "is" "green" "+") ("something" "is" "round" "+")) -> ("something" "is" "blue" "+"))
Green things are blue.
((("something" "is" "green" "+")) -> ("something" "is" "blue" "+"))
Smart, blue things are not nice.
((("something" "is" "smart" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "-"))
If Bob is kind and Bob is smart then Bob is green.
((("Bob" "is" "kind" "+") ("Bob" "is" "smart" "+")) -> ("Bob" "is" "green" "+"))
If Harry is kind and Harry is blue then Harry is not smart.
((("Harry" "is" "kind" "+") ("Harry" "is" "blue" "+")) -> ("Harry" "is" "smart" "-"))
If Bob is smart and Bob is blue then Bob is round.
((("Bob" "is" "smart" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "round" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Bob is not nice.
False
1
inv-proof
[(triple1)]
("Bob" "is" "nice" "-")
triple1
Harry is green.
True
3
proof
[(((triple7 triple6) -> rule1))]
("Harry" "is" "green" "+")
((triple7 triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
3
inv-proof
[(((triple7 triple6) -> rule1))]
("Harry" "is" "green" "-")
((triple7 triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
True
4
proof
[(((((triple7 triple6) -> rule1)) -> rule4) OR ((((triple7 triple6) -> rule1) triple5) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule3))]
("Harry" "is" "blue" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not blue.
False
4
inv-proof
[(((((triple7 triple6) -> rule1)) -> rule4) OR ((((triple7 triple6) -> rule1) triple5) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule3))]
("Harry" "is" "blue" "-")
((((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not smart.
True
6
proof
[(((triple4 ((((triple7 triple6) -> rule1)) -> rule4)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple5) -> rule2)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple7) -> rule3)) -> rule7))]
("Harry" "is" "smart" "-")
((triple4 ((((triple7 triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple5) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is smart.
False
6
inv-proof
[(((triple4 ((((triple7 triple6) -> rule1)) -> rule4)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple5) -> rule2)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple7) -> rule3)) -> rule7))]
("Harry" "is" "smart" "+")
((triple4 ((((triple7 triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple5) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is not blue.
Unknown
inv-rconc
[@2: Bob is blue.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "blue" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Charlie is not blue.
Unknown
inv-rconc
[@2: Charlie is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is green.
Unknown
rconc
[@1: Charlie is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "green" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is round.
Unknown
random
[@0: Charlie is round.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "round" "+")
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is kind.
Unknown
random
[@0: Charlie is kind.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "kind" "+")
@0: Bob is nice.[(triple1)] Bob is round.[(triple2)] Charlie is quiet.[(triple3)] Harry is kind.[(triple4)] Harry is nice.[(triple5)] Harry is quiet.[(triple6)] Harry is round.[(triple7)] @1: Harry is green.[(((triple7 triple6) -> rule1))] @2: Harry is blue.[(((((triple7 triple6) -> rule1)) -> rule4) OR ((((triple7 triple6) -> rule1) triple5) -> rule2) OR ((((triple7 triple6) -> rule1) triple7) -> rule3))] @3: Harry is not smart.[(((triple4 ((((triple7 triple6) -> rule1)) -> rule4)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple5) -> rule2)) -> rule7) OR ((triple4 ((((triple7 triple6) -> rule1) triple7) -> rule3)) -> rule7))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is round.
("Bob" "is" "round" "+")
triple2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple3
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Harry is green.
("Harry" "is" "green" "+")
((triple7 triple6) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((((triple7 triple6) -> (rule1 % int2))) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple5) -> (rule2 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((triple7 triple6) -> (rule1 % int2)) triple7) -> (rule3 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not smart.
("Harry" "is" "smart" "-")
((triple4 ((((triple7 triple6) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple5) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((triple4 ((((triple7 triple6) -> (rule1 % int3)) triple7) -> (rule3 % int2))) -> (rule7 % int1))
Harry is not smart.
("Harry" "is" "smart" "-")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3