Bob is smart. Erin is furry. Fiona is furry. Harry is green. If someone is round then they are big. If someone is quiet and furry then they are green. All furry people are quiet.
Bob is smart.
("Bob" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
If someone is quiet and furry then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
All furry people are quiet.
((("someone" "is" "furry" "+")) -> ("someone" "is" "quiet" "+"))
Harry is green.
True
1
proof
[(triple4)]
("Harry" "is" "green" "+")
triple4
Harry is not green.
False
1
inv-proof
[(triple4)]
("Harry" "is" "green" "-")
triple4
Erin is quiet.
True
2
proof
[(((triple2) -> rule3))]
("Erin" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is not quiet.
False
2
inv-proof
[(((triple2) -> rule3))]
("Erin" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is green.
True
4
proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Fiona" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((((triple3) -> rule3) triple3) -> rule2))]
("Fiona" "is" "green" "-")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "green" "-")
Bob is quiet.
Unknown
rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "quiet" "+")
Erin is not big.
Unknown
inv-rconc
[@1: Erin is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "big" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
@0: Bob is smart.[(triple1)] Erin is furry.[(triple2)] Fiona is furry.[(triple3)] Harry is green.[(triple4)] @1: Erin is quiet.[(((triple2) -> rule3))] Fiona is quiet.[(((triple3) -> rule3))] @2: Erin is green.[(((((triple2) -> rule3) triple2) -> rule2))] Fiona is green.[(((((triple3) -> rule3) triple3) -> rule2))]
Bob is smart.
("Bob" "is" "smart" "+")
triple1
Erin is furry.
("Erin" "is" "furry" "+")
triple2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple2) -> (rule3 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule3 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((((triple2) -> (rule3 % int2)) triple2) -> (rule2 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple3) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2