Bob is kind. Bob is not quiet. Bob is smart. Dave is blue. Dave is nice. Dave is quiet. Dave is rough. Fiona is nice. Fiona is white. Gary is blue. Gary is kind. Gary is nice. Gary is quiet. Gary is rough. Gary is smart. Gary is not white. If Dave is kind then Dave is blue. Smart things are nice. If something is quiet then it is blue. All kind, nice things are blue. If Fiona is smart then Fiona is rough. If something is white then it is kind. If something is nice then it is smart. If Dave is not rough then Dave is not white.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Bob is smart.
("Bob" "is" "smart" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is not white.
("Gary" "is" "white" "-")
If Dave is kind then Dave is blue.
((("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "+"))
Smart things are nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is quiet then it is blue.
((("something" "is" "quiet" "+")) -> ("something" "is" "blue" "+"))
All kind, nice things are blue.
((("something" "is" "kind" "+") ("something" "is" "nice" "+")) -> ("something" "is" "blue" "+"))
If Fiona is smart then Fiona is rough.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "rough" "+"))
If something is white then it is kind.
((("something" "is" "white" "+")) -> ("something" "is" "kind" "+"))
If something is nice then it is smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If Dave is not rough then Dave is not white.
((("Dave" "is" "rough" "~")) -> ("Dave" "is" "white" "-"))
Gary is nice.
True
1
proof
[(triple12 OR ((triple15) -> rule2))]
("Gary" "is" "nice" "+")
triple12
((triple15) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple15 OR ((triple12) -> rule7))]
("Gary" "is" "smart" "-")
triple15
((triple12) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Fiona is kind.
True
2
proof
[(((triple9) -> rule6))]
("Fiona" "is" "kind" "+")
((triple9) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Bob is not nice.
False
2
inv-proof
[(((triple3) -> rule2))]
("Bob" "is" "nice" "-")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Fiona is blue.
True
4
proof
[(((((triple9) -> rule6) triple8) -> rule4))]
("Fiona" "is" "blue" "+")
((((triple9) -> (rule6 % int2)) triple8) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not rough.
False
3
inv-proof
[(((((triple8) -> rule7)) -> rule5))]
("Fiona" "is" "rough" "-")
((((triple8) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Dave" "is" "kind" "-")
Dave is white.
Unknown
random
[@0: Dave is white.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "white" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is kind.[(triple1)] Bob is not quiet.[(triple2)] Bob is smart.[(triple3)] Dave is blue.[(triple4 OR ((triple6) -> rule3))] Dave is nice.[(triple5)] Dave is quiet.[(triple6)] Dave is rough.[(triple7)] Fiona is nice.[(triple8)] Fiona is white.[(triple9)] Gary is blue.[(triple10 OR ((triple13) -> rule3) OR ((triple11 triple12) -> rule4) OR ((triple11 ((triple15) -> rule2)) -> rule4))] Gary is kind.[(triple11)] Gary is nice.[(triple12 OR ((triple15) -> rule2))] Gary is not white.[(triple16)] Gary is quiet.[(triple13)] Gary is rough.[(triple14)] Gary is smart.[(triple15 OR ((triple12) -> rule7))] @1: Bob is nice.[(((triple3) -> rule2))] Dave is smart.[(((triple5) -> rule7))] Fiona is kind.[(((triple9) -> rule6))] Fiona is smart.[(((triple8) -> rule7))] @2: Bob is blue.[(((triple1 ((triple3) -> rule2)) -> rule4))] Fiona is blue.[(((((triple9) -> rule6) triple8) -> rule4))] Fiona is rough.[(((((triple8) -> rule7)) -> rule5))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Bob is smart.
("Bob" "is" "smart" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
((triple6) -> (rule3 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
triple5
Dave is quiet.
("Dave" "is" "quiet" "+")
triple6
Dave is rough.
("Dave" "is" "rough" "+")
triple7
Fiona is nice.
("Fiona" "is" "nice" "+")
triple8
Fiona is white.
("Fiona" "is" "white" "+")
triple9
Gary is blue.
("Gary" "is" "blue" "+")
triple10
((triple13) -> (rule3 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple11 triple12) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
((triple11 ((triple15) -> (rule2 % int2))) -> (rule4 % int1))
Gary is blue.
("Gary" "is" "blue" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is nice.
("Gary" "is" "nice" "+")
triple12
((triple15) -> (rule2 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is not white.
("Gary" "is" "white" "-")
triple16
Gary is quiet.
("Gary" "is" "quiet" "+")
triple13
Gary is rough.
("Gary" "is" "rough" "+")
triple14
Gary is smart.
("Gary" "is" "smart" "+")
triple15
((triple12) -> (rule7 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple5) -> (rule7 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple9) -> (rule6 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple8) -> (rule7 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((triple1 ((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Fiona is blue.
("Fiona" "is" "blue" "+")
((((triple9) -> (rule6 % int2)) triple8) -> (rule4 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((((triple8) -> (rule7 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2