Bob is quiet. Erin is young. Fiona is rough. If someone is smart and rough then they are cold. If someone is green and white then they are cold. All cold, quiet people are smart. If someone is young and quiet then they are not smart. Young people are green. If someone is white and cold then they are not green. If someone is green and not rough then they are quiet. All green people are quiet.
Bob is quiet.
("Bob" "is" "quiet" "+")
Erin is young.
("Erin" "is" "young" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
If someone is smart and rough then they are cold.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "cold" "+"))
If someone is green and white then they are cold.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "cold" "+"))
All cold, quiet people are smart.
((("someone" "is" "cold" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If someone is young and quiet then they are not smart.
((("someone" "is" "young" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "-"))
Young people are green.
((("someone" "is" "young" "+")) -> ("someone" "is" "green" "+"))
If someone is white and cold then they are not green.
((("someone" "is" "white" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "green" "-"))
If someone is green and not rough then they are quiet.
((("someone" "is" "green" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "quiet" "+"))
All green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Erin is young.
True
1
proof
[(triple2)]
("Erin" "is" "young" "+")
triple2
Fiona is not rough.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "rough" "-")
triple3
Erin is green.
True
2
proof
[(((triple2) -> rule5))]
("Erin" "is" "green" "+")
((triple2) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
2
inv-proof
[(((triple2) -> rule5))]
("Erin" "is" "green" "-")
((triple2) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
True
3
proof
[(((((triple2) -> rule5)) -> rule8))]
("Erin" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not quiet.
False
3
inv-proof
[(((((triple2) -> rule5)) -> rule8))]
("Erin" "is" "quiet" "-")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not smart.
True
5
proof
[(((triple2 ((((triple2) -> rule5)) -> rule8)) -> rule4))]
("Erin" "is" "smart" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is smart.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule5)) -> rule8)) -> rule4))]
("Erin" "is" "smart" "+")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Fiona is cold.
Unknown
rconc
[@3: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "cold" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Fiona" "is" "smart" "-")
Erin is cold.
Unknown
rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "cold" "+")
Bob is not white.
Unknown
inv-random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Erin is not rough.
Unknown
inv-random
[@0: Erin is rough.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is quiet.[(triple1)] Erin is young.[(triple2)] Fiona is rough.[(triple3)] @1: Erin is green.[(((triple2) -> rule5))] @2: Erin is quiet.[(((((triple2) -> rule5)) -> rule8))] @3: Erin is not smart.[(((triple2 ((((triple2) -> rule5)) -> rule8)) -> rule4))]
Bob is quiet.
("Bob" "is" "quiet" "+")
triple1
Erin is young.
("Erin" "is" "young" "+")
triple2
Fiona is rough.
("Fiona" "is" "rough" "+")
triple3
Erin is green.
("Erin" "is" "green" "+")
((triple2) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
((((triple2) -> (rule5 % int2))) -> (rule8 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is not smart.
("Erin" "is" "smart" "-")
((triple2 ((((triple2) -> (rule5 % int3))) -> (rule8 % int2))) -> (rule4 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1
Erin is quiet.
("Erin" "is" "quiet" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3