Bob is furry. Bob is kind. Dave is furry. Dave is not kind. Fiona is furry. Fiona is green. Fiona is nice. Fiona is quiet. Harry is cold. Harry is not nice. Harry is quiet. Harry is white. If something is nice and not kind then it is quiet. All green, kind things are not quiet. Nice things are quiet. If something is quiet then it is green. If something is kind then it is green. If Harry is cold and Harry is not furry then Harry is not white. If something is kind and nice then it is cold. If something is nice and not quiet then it is not cold.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is not nice.
("Harry" "is" "nice" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is nice and not kind then it is quiet.
((("something" "is" "nice" "+") ("something" "is" "kind" "~")) -> ("something" "is" "quiet" "+"))
All green, kind things are not quiet.
((("something" "is" "green" "+") ("something" "is" "kind" "+")) -> ("something" "is" "quiet" "-"))
Nice things are quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
If something is quiet then it is green.
((("something" "is" "quiet" "+")) -> ("something" "is" "green" "+"))
If something is kind then it is green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Harry is cold and Harry is not furry then Harry is not white.
((("Harry" "is" "cold" "+") ("Harry" "is" "furry" "~")) -> ("Harry" "is" "white" "-"))
If something is kind and nice then it is cold.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "cold" "+"))
If something is nice and not quiet then it is not cold.
((("something" "is" "nice" "+") ("something" "is" "quiet" "~")) -> ("something" "is" "cold" "-"))
Dave is not kind.
True
1
proof
[(triple4)]
("Dave" "is" "kind" "-")
triple4
Harry is nice.
False
1
inv-proof
[(triple10)]
("Harry" "is" "nice" "+")
triple10
Harry is green.
True
2
proof
[(((triple11) -> rule4))]
("Harry" "is" "green" "+")
((triple11) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple11) -> rule4))]
("Harry" "is" "green" "-")
((triple11) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is not quiet.
True
4
proof
[(((((triple2) -> rule5) triple2) -> rule2))]
("Bob" "is" "quiet" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is quiet.
False
4
inv-proof
[(((((triple2) -> rule5) triple2) -> rule2))]
("Bob" "is" "quiet" "+")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@2: Dave is green.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not quiet.
Unknown
inv-rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "quiet" "-")
Harry is kind.
Unknown
random
[@0: Harry is kind.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not kind.
Unknown
inv-random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Bob is furry.[(triple1)] Bob is kind.[(triple2)] Dave is furry.[(triple3)] Dave is not kind.[(triple4)] Fiona is furry.[(triple5)] Fiona is green.[(triple6 OR ((triple8) -> rule4) OR ((((triple7) -> rule3)) -> rule4))] Fiona is nice.[(triple7)] Fiona is quiet.[(triple8 OR ((triple7) -> rule3))] Harry is cold.[(triple9)] Harry is not nice.[(triple10)] Harry is quiet.[(triple11)] Harry is white.[(triple12)] @1: Bob is green.[(((triple2) -> rule5))] Harry is green.[(((triple11) -> rule4))] @2: Bob is not quiet.[(((((triple2) -> rule5) triple2) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is not kind.
("Dave" "is" "kind" "-")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is green.
("Fiona" "is" "green" "+")
triple6
((triple8) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
((((triple7) -> (rule3 % int2))) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple7
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple8
((triple7) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple9
Harry is not nice.
("Harry" "is" "nice" "-")
triple10
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule5 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple11) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Bob is not quiet.
("Bob" "is" "quiet" "-")
((((triple2) -> (rule5 % int2)) triple2) -> (rule2 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is green.
("Bob" "is" "green" "+")
int2