Bob is white. Erin is quiet. Fiona is nice. Harry is quiet. If Erin is nice then Erin is white. If someone is nice and white then they are not green. If someone is quiet and nice then they are green. If Harry is quiet then Harry is blue. Nice people are quiet. All blue people are white. If someone is round and white then they are blue. If someone is white then they are round.
Bob is white.
("Bob" "is" "white" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Erin is nice then Erin is white.
((("Erin" "is" "nice" "+")) -> ("Erin" "is" "white" "+"))
If someone is nice and white then they are not green.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "-"))
If someone is quiet and nice then they are green.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
If Harry is quiet then Harry is blue.
((("Harry" "is" "quiet" "+")) -> ("Harry" "is" "blue" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All blue people are white.
((("someone" "is" "blue" "+")) -> ("someone" "is" "white" "+"))
If someone is round and white then they are blue.
((("someone" "is" "round" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "blue" "+"))
If someone is white then they are round.
((("someone" "is" "white" "+")) -> ("someone" "is" "round" "+"))
Erin is quiet.
True
1
proof
[(triple2)]
("Erin" "is" "quiet" "+")
triple2
Bob is not white.
False
1
inv-proof
[(triple1)]
("Bob" "is" "white" "-")
triple1
Bob is round.
True
2
proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is not round.
False
2
inv-proof
[(((triple1) -> rule8))]
("Bob" "is" "round" "-")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is green.
True
4
proof
[(((((triple3) -> rule5) triple3) -> rule3))]
("Fiona" "is" "green" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((((triple3) -> rule5) triple3) -> rule3))]
("Fiona" "is" "green" "-")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Harry is round.
True
4
proof
[(((((((triple4) -> rule4)) -> rule6)) -> rule8))]
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Harry is not round.
False
4
inv-proof
[(((((((triple4) -> rule4)) -> rule6)) -> rule8))]
("Harry" "is" "round" "-")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "quiet" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "green" "+")
Fiona is not round.
Unknown
inv-rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule8 <- rule6 <- rule7 <- FAIL)]]
("Fiona" "is" "round" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Erin is not nice.
Unknown
inv-random
[@0: Erin is nice.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "nice" "-")
Fiona is smart.
Unknown
random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "+")
@0: Bob is white.[(triple1)] Erin is quiet.[(triple2)] Fiona is nice.[(triple3)] Harry is quiet.[(triple4)] @1: Bob is round.[(((triple1) -> rule8))] Fiona is quiet.[(((triple3) -> rule5))] Harry is blue.[(((triple4) -> rule4))] @2: Bob is blue.[(((((triple1) -> rule8) triple1) -> rule7))] Fiona is green.[(((((triple3) -> rule5) triple3) -> rule3))] Harry is white.[(((((triple4) -> rule4)) -> rule6))] @3: Harry is round.[(((((((triple4) -> rule4)) -> rule6)) -> rule8))]
Bob is white.
("Bob" "is" "white" "+")
triple1
Erin is quiet.
("Erin" "is" "quiet" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule8 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((triple3) -> (rule5 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
((triple4) -> (rule4 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
((((triple1) -> (rule8 % int2)) triple1) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Fiona is green.
("Fiona" "is" "green" "+")
((((triple3) -> (rule5 % int2)) triple3) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple4) -> (rule4 % int2))) -> (rule6 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((((((triple4) -> (rule4 % int3))) -> (rule6 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
int3