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