Bob is nice. Bob is quiet. Bob is red. Bob is round. Bob is white. Bob is young. Erin is furry. Erin is nice. Erin is quiet. Erin is red. Erin is round. Erin is young. Fiona is nice. Fiona is quiet. Fiona is white. Fiona is not young. White people are red. If Bob is red then Bob is nice. All white people are nice. If Erin is round and Erin is nice then Erin is young. All quiet, nice people are round. All round, furry people are quiet. Round, young people are quiet. If someone is round and not nice then they are furry.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is white.
("Bob" "is" "white" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is red.
("Erin" "is" "red" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is not young.
("Fiona" "is" "young" "-")
White people are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
If Bob is red then Bob is nice.
((("Bob" "is" "red" "+")) -> ("Bob" "is" "nice" "+"))
All white people are nice.
((("someone" "is" "white" "+")) -> ("someone" "is" "nice" "+"))
If Erin is round and Erin is nice then Erin is young.
((("Erin" "is" "round" "+") ("Erin" "is" "nice" "+")) -> ("Erin" "is" "young" "+"))
All quiet, nice people are round.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
All round, furry people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Round, young people are quiet.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
If someone is round and not nice then they are furry.
((("someone" "is" "round" "+") ("someone" "is" "nice" "~")) -> ("someone" "is" "furry" "+"))
Fiona is nice.
True
1
proof
[(triple13 OR ((triple15) -> rule3))]
("Fiona" "is" "nice" "+")
triple13
((triple15) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not nice.
False
1
inv-proof
[(triple13 OR ((triple15) -> rule3))]
("Fiona" "is" "nice" "-")
triple13
((triple15) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is round.
True
3
proof
[(((triple14 triple13) -> rule5) OR ((triple14 ((triple15) -> rule3)) -> rule5))]
("Fiona" "is" "round" "+")
((triple14 triple13) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple14 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Fiona is not red.
False
2
inv-proof
[(((triple15) -> rule1))]
("Fiona" "is" "red" "-")
((triple15) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "furry" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "furry" "+")
@0: Bob is nice.[(triple1 OR ((triple3) -> rule2) OR ((triple5) -> rule3) OR ((((triple5) -> rule1)) -> rule2))] Bob is quiet.[(triple2 OR ((triple4 triple6) -> rule7))] Bob is red.[(triple3 OR ((triple5) -> rule1))] Bob is round.[(triple4 OR ((triple2 triple1) -> rule5) OR ((triple2 ((triple3) -> rule2)) -> rule5) OR ((triple2 ((triple5) -> rule3)) -> rule5) OR ((triple2 ((((triple5) -> rule1)) -> rule2)) -> rule5))] Bob is white.[(triple5)] Bob is young.[(triple6)] Erin is furry.[(triple7)] Erin is nice.[(triple8)] Erin is quiet.[(triple9 OR ((triple11 triple12) -> rule7) OR ((triple11 triple7) -> rule6) OR ((triple11 ((triple11 triple8) -> rule4)) -> rule7))] Erin is red.[(triple10)] Erin is round.[(triple11 OR ((triple9 triple8) -> rule5))] Erin is young.[(triple12 OR ((triple11 triple8) -> rule4) OR ((((triple9 triple8) -> rule5) triple8) -> rule4))] Fiona is nice.[(triple13 OR ((triple15) -> rule3))] Fiona is not young.[(triple16)] Fiona is quiet.[(triple14)] Fiona is white.[(triple15)] @1: Fiona is red.[(((triple15) -> rule1))] Fiona is round.[(((triple14 triple13) -> rule5) OR ((triple14 ((triple15) -> rule3)) -> rule5))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
((triple3) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple5) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple5) -> (rule1 % int2))) -> (rule2 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
((triple4 triple6) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
((triple5) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple2 triple1) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple2 ((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((triple5) -> (rule3 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((triple2 ((((triple5) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule5 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
triple5
Bob is young.
("Bob" "is" "young" "+")
triple6
Erin is furry.
("Erin" "is" "furry" "+")
triple7
Erin is nice.
("Erin" "is" "nice" "+")
triple8
Erin is quiet.
("Erin" "is" "quiet" "+")
triple9
((triple11 triple12) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 triple7) -> (rule6 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((triple11 ((triple11 triple8) -> (rule4 % int2))) -> (rule7 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
triple10
Erin is round.
("Erin" "is" "round" "+")
triple11
((triple9 triple8) -> (rule5 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
triple12
((triple11 triple8) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
((((triple9 triple8) -> (rule5 % int2)) triple8) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple13
((triple15) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
triple16
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple14
Fiona is white.
("Fiona" "is" "white" "+")
triple15
Fiona is red.
("Fiona" "is" "red" "+")
((triple15) -> (rule1 % int1))
Fiona is red.
("Fiona" "is" "red" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((triple14 triple13) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
((triple14 ((triple15) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2