Bob is nice. Bob is not quiet. Dave is green. Dave is nice. Dave is round. Dave is not smart. Dave is not white. Dave is young. Erin is nice. Erin is quiet. Erin is round. Erin is smart. Fiona is nice. Fiona is not round. Fiona is smart. Fiona is white. Round, smart things are white. If Bob is white then Bob is smart. Nice things are young.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is not quiet.
("Bob" "is" "quiet" "-")
Dave is green.
("Dave" "is" "green" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is not smart.
("Dave" "is" "smart" "-")
Dave is not white.
("Dave" "is" "white" "-")
Dave is young.
("Dave" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Round, smart things are white.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
If Bob is white then Bob is smart.
((("Bob" "is" "white" "+")) -> ("Bob" "is" "smart" "+"))
Nice things are young.
((("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
Dave is young.
True
1
proof
[(triple8 OR ((triple4) -> rule3))]
("Dave" "is" "young" "+")
triple8
((triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is not quiet.
False
1
inv-proof
[(triple10)]
("Erin" "is" "quiet" "-")
triple10
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is nice.[(triple1)] Bob is not quiet.[(triple2)] Dave is green.[(triple3)] Dave is nice.[(triple4)] Dave is not smart.[(triple6)] Dave is not white.[(triple7)] Dave is round.[(triple5)] Dave is young.[(triple8 OR ((triple4) -> rule3))] Erin is nice.[(triple9)] Erin is quiet.[(triple10)] Erin is round.[(triple11)] Erin is smart.[(triple12)] Fiona is nice.[(triple13)] Fiona is not round.[(triple14)] Fiona is smart.[(triple15)] Fiona is white.[(triple16)] @1: Bob is young.[(((triple1) -> rule3))] Erin is white.[(((triple11 triple12) -> rule1))] Erin is young.[(((triple9) -> rule3))] Fiona is young.[(((triple13) -> rule3))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is not quiet.
("Bob" "is" "quiet" "-")
triple2
Dave is green.
("Dave" "is" "green" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is not smart.
("Dave" "is" "smart" "-")
triple6
Dave is not white.
("Dave" "is" "white" "-")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple8
((triple4) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
triple9
Erin is quiet.
("Erin" "is" "quiet" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
Erin is smart.
("Erin" "is" "smart" "+")
triple12
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
Fiona is not round.
("Fiona" "is" "round" "-")
triple14
Fiona is smart.
("Fiona" "is" "smart" "+")
triple15
Fiona is white.
("Fiona" "is" "white" "+")
triple16
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
((triple11 triple12) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple9) -> (rule3 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple13) -> (rule3 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1