Bob is blue. Bob is green. Charlie is not quiet. Dave is not blue. Harry is nice. Harry is round. Harry is not young. Nice people are blue. All green people are round. If someone is furry and not nice then they are round. All young, green people are round. If Bob is young and Bob is quiet then Bob is round. If someone is blue then they are quiet.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is green.
("Bob" "is" "green" "+")
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
Dave is not blue.
("Dave" "is" "blue" "-")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is not young.
("Harry" "is" "young" "-")
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
All green people are round.
((("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is furry and not nice then they are round.
((("someone" "is" "furry" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "round" "+"))
All young, green people are round.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If Bob is young and Bob is quiet then Bob is round.
((("Bob" "is" "young" "+") ("Bob" "is" "quiet" "+")) -> ("Bob" "is" "round" "+"))
If someone is blue then they are quiet.
((("someone" "is" "blue" "+")) -> ("someone" "is" "quiet" "+"))
Charlie is not quiet.
True
1
proof
[(triple3)]
("Charlie" "is" "quiet" "-")
triple3
Bob is not green.
False
1
inv-proof
[(triple2)]
("Bob" "is" "green" "-")
triple2
Harry is blue.
True
2
proof
[(((triple5) -> rule1))]
("Harry" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "quiet" "-")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is quiet.
True
3
proof
[(((((triple5) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not quiet.
False
3
inv-proof
[(((((triple5) -> rule1)) -> rule6))]
("Harry" "is" "quiet" "-")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Charlie is not blue.
Unknown
inv-rconc
[@1: Charlie is blue.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Charlie" "is" "blue" "-")
Charlie is round.
Unknown
rconc
[@1: Charlie is round.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "round" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "quiet" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Dave is not green.
Unknown
inv-random
[@0: Dave is green.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "green" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is green.[(triple2)] Charlie is not quiet.[(triple3)] Dave is not blue.[(triple4)] Harry is nice.[(triple5)] Harry is not young.[(triple7)] Harry is round.[(triple6)] @1: Bob is quiet.[(((triple1) -> rule6))] Bob is round.[(((triple2) -> rule2))] Harry is blue.[(((triple5) -> rule1))] @2: Harry is quiet.[(((((triple5) -> rule1)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
triple3
Dave is not blue.
("Dave" "is" "blue" "-")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
Harry is not young.
("Harry" "is" "young" "-")
triple7
Harry is round.
("Harry" "is" "round" "+")
triple6
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule2 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple5) -> (rule1 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
((((triple5) -> (rule1 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2