Bob is green. Bob is not white. Charlie is big. Charlie is not rough. Charlie is smart. Erin is smart. Fiona is white. If someone is furry and not white then they are not rough. If someone is green and not furry then they are rough. Furry people are green. If someone is white then they are green. All smart people are not green. If someone is rough and not furry then they are green. If someone is green then they are quiet. All green people are quiet.
Bob is green.
("Bob" "is" "green" "+")
Bob is not white.
("Bob" "is" "white" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is not rough.
("Charlie" "is" "rough" "-")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
If someone is furry and not white then they are not rough.
((("someone" "is" "furry" "+") ("someone" "is" "white" "~")) -> ("someone" "is" "rough" "-"))
If someone is green and not furry then they are rough.
((("someone" "is" "green" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "rough" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is white then they are green.
((("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
All smart people are not green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "-"))
If someone is rough and not furry then they are green.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "green" "+"))
If someone is green then they are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Erin is smart.
True
1
proof
[(triple6)]
("Erin" "is" "smart" "+")
triple6
Charlie is not smart.
False
1
inv-proof
[(triple5)]
("Charlie" "is" "smart" "-")
triple5
Fiona is green.
True
2
proof
[(((triple7) -> rule4))]
("Fiona" "is" "green" "+")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Charlie is green.
False
2
inv-proof
[(((triple5) -> rule5))]
("Charlie" "is" "green" "+")
((triple5) -> (rule5 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Fiona is quiet.
True
3
proof
[(((((triple7) -> rule4)) -> rule7) OR ((((triple7) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "+")
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is not quiet.
False
3
inv-proof
[(((((triple7) -> rule4)) -> rule7) OR ((((triple7) -> rule4)) -> rule8))]
("Fiona" "is" "quiet" "-")
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "rough" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Erin" "is" "quiet" "+")
Erin is not rough.
Unknown
inv-rconc
[@1: Erin is rough.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "rough" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Bob is big.
Unknown
random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "+")
@0: Bob is green.[(triple1)] Bob is not white.[(triple2)] Charlie is big.[(triple3)] Charlie is not rough.[(triple4)] Charlie is smart.[(triple5)] Erin is smart.[(triple6)] Fiona is white.[(triple7)] @1: Bob is quiet.[(((triple1) -> rule7) OR ((triple1) -> rule8))] Charlie is not green.[(((triple5) -> rule5))] Erin is not green.[(((triple6) -> rule5))] Fiona is green.[(((triple7) -> rule4))] @2: Fiona is quiet.[(((((triple7) -> rule4)) -> rule7) OR ((((triple7) -> rule4)) -> rule8))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is not white.
("Bob" "is" "white" "-")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
triple3
Charlie is not rough.
("Charlie" "is" "rough" "-")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
Fiona is white.
("Fiona" "is" "white" "+")
triple7
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple1) -> (rule7 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
((triple1) -> (rule8 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Charlie is not green.
("Charlie" "is" "green" "-")
((triple5) -> (rule5 % int1))
Charlie is not green.
("Charlie" "is" "green" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
((triple6) -> (rule5 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple7) -> (rule4 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is quiet.
("Fiona" "is" "quiet" "+")
((((triple7) -> (rule4 % int2))) -> (rule7 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
((((triple7) -> (rule4 % int2))) -> (rule8 % int1))
Fiona is quiet.
("Fiona" "is" "quiet" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2