Bob is green. Erin is kind. Fiona is smart. If something is kind and not smart then it is green. If something is smart and white then it is red. All smart things are round. All red things are kind. If Erin is not green then Erin is round. All red things are young. If something is round then it is not young. If Erin is not round then Erin is not young.
Bob is green.
("Bob" "is" "green" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
If something is kind and not smart then it is green.
((("something" "is" "kind" "+") ("something" "is" "smart" "~")) -> ("something" "is" "green" "+"))
If something is smart and white then it is red.
((("something" "is" "smart" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All red things are kind.
((("something" "is" "red" "+")) -> ("something" "is" "kind" "+"))
If Erin is not green then Erin is round.
((("Erin" "is" "green" "~")) -> ("Erin" "is" "round" "+"))
All red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If something is round then it is not young.
((("something" "is" "round" "+")) -> ("something" "is" "young" "-"))
If Erin is not round then Erin is not young.
((("Erin" "is" "round" "~")) -> ("Erin" "is" "young" "-"))
Fiona is smart.
True
1
proof
[(triple3)]
("Fiona" "is" "smart" "+")
triple3
Erin is not kind.
False
1
inv-proof
[(triple2)]
("Erin" "is" "kind" "-")
triple2
Fiona is round.
True
2
proof
[(((triple3) -> rule3))]
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not round.
False
2
inv-proof
[(((triple3) -> rule3))]
("Fiona" "is" "round" "-")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not young.
True
3
proof
[(((((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "young" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is young.
False
3
inv-proof
[(((((triple3) -> rule3)) -> rule7))]
("Fiona" "is" "young" "+")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "red" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not kind.
Unknown
inv-rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Erin is not smart.
Unknown
inv-random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Bob is green.[(triple1)] Erin is kind.[(triple2)] Fiona is smart.[(triple3)] @1: Fiona is round.[(((triple3) -> rule3))] @2: Fiona is not young.[(((((triple3) -> rule3)) -> rule7))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is kind.
("Erin" "is" "kind" "+")
triple2
Fiona is smart.
("Fiona" "is" "smart" "+")
triple3
Fiona is round.
("Fiona" "is" "round" "+")
((triple3) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
((((triple3) -> (rule3 % int2))) -> (rule7 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2