Bob is nice. Bob is quiet. Bob is not white. Erin is nice. Erin is quiet. Erin is round. Fiona is big. Fiona is white. Harry is big. Harry is nice. Harry is quiet. Harry is white. Quiet people are round. Big, round people are nice. All nice people are not blue.
Bob is nice.
("Bob" "is" "nice" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is not white.
("Bob" "is" "white" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is white.
("Harry" "is" "white" "+")
Quiet people are round.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "round" "+"))
Big, round people are nice.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
All nice people are not blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "-"))
Bob is quiet.
True
1
proof
[(triple2)]
("Bob" "is" "quiet" "+")
triple2
Harry is not quiet.
False
1
inv-proof
[(triple11)]
("Harry" "is" "quiet" "-")
triple11
Harry is not blue.
True
2
proof
[(((triple10) -> rule3) OR ((((triple9 ((triple11) -> rule1)) -> rule2)) -> rule3))]
("Harry" "is" "blue" "-")
((triple10) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
((((triple9 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Bob is not round.
False
2
inv-proof
[(((triple2) -> rule1))]
("Bob" "is" "round" "-")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is nice.
Unknown
rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is nice.[(triple1)] Bob is not white.[(triple3)] Bob is quiet.[(triple2)] Erin is nice.[(triple4)] Erin is quiet.[(triple5)] Erin is round.[(triple6 OR ((triple5) -> rule1))] Fiona is big.[(triple7)] Fiona is white.[(triple8)] Harry is big.[(triple9)] Harry is nice.[(triple10 OR ((triple9 ((triple11) -> rule1)) -> rule2))] Harry is quiet.[(triple11)] Harry is white.[(triple12)] @1: Bob is not blue.[(((triple1) -> rule3))] Bob is round.[(((triple2) -> rule1))] Erin is not blue.[(((triple4) -> rule3))] Harry is not blue.[(((triple10) -> rule3) OR ((((triple9 ((triple11) -> rule1)) -> rule2)) -> rule3))] Harry is round.[(((triple11) -> rule1))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
triple5
Erin is round.
("Erin" "is" "round" "+")
triple6
((triple5) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple7
Fiona is white.
("Fiona" "is" "white" "+")
triple8
Harry is big.
("Harry" "is" "big" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple9 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Harry is white.
("Harry" "is" "white" "+")
triple12
Bob is not blue.
("Bob" "is" "blue" "-")
((triple1) -> (rule3 % int1))
Bob is not blue.
("Bob" "is" "blue" "-")
int1
Bob is round.
("Bob" "is" "round" "+")
((triple2) -> (rule1 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Erin is not blue.
("Erin" "is" "blue" "-")
((triple4) -> (rule3 % int1))
Erin is not blue.
("Erin" "is" "blue" "-")
int1
Harry is not blue.
("Harry" "is" "blue" "-")
((triple10) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
((((triple9 ((triple11) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Harry is not blue.
("Harry" "is" "blue" "-")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
((triple11) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1