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