Dave is smart. Fiona is kind. If someone is kind and rough then they are green. All smart people are green. Kind people are white. All rough, green people are round. If someone is kind then they are rough. All smart, round people are nice.
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
If someone is kind and rough then they are green.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
All smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
Kind people are white.
((("someone" "is" "kind" "+")) -> ("someone" "is" "white" "+"))
All rough, green people are round.
((("someone" "is" "rough" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
If someone is kind then they are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
All smart, round people are nice.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
Dave is smart.
True
1
proof
[(triple1)]
("Dave" "is" "smart" "+")
triple1
Fiona is not kind.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "kind" "-")
triple2
Fiona is rough.
True
2
proof
[(((triple2) -> rule5))]
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple2) -> rule3))]
("Fiona" "is" "white" "-")
((triple2) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
True
4
proof
[(((triple2 ((triple2) -> rule5)) -> rule1))]
("Fiona" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not green.
False
4
inv-proof
[(((triple2 ((triple2) -> rule5)) -> rule1))]
("Fiona" "is" "green" "-")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
True
7
proof
[(((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule1)) -> rule4))]
("Fiona" "is" "round" "+")
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not round.
False
7
inv-proof
[(((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule1)) -> rule4))]
("Fiona" "is" "round" "-")
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Dave is not rough.
Unknown
inv-rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Dave" "is" "rough" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "nice" "+")
Dave is not round.
Unknown
inv-rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Dave" "is" "round" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Dave is kind.
Unknown
random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "+")
@0: Dave is smart.[(triple1)] Fiona is kind.[(triple2)] @1: Dave is green.[(((triple1) -> rule2))] Fiona is rough.[(((triple2) -> rule5))] Fiona is white.[(((triple2) -> rule3))] @2: Fiona is green.[(((triple2 ((triple2) -> rule5)) -> rule1))] @3: Fiona is round.[(((((triple2) -> rule5) ((triple2 ((triple2) -> rule5)) -> rule1)) -> rule4))]
Dave is smart.
("Dave" "is" "smart" "+")
triple1
Fiona is kind.
("Fiona" "is" "kind" "+")
triple2
Dave is green.
("Dave" "is" "green" "+")
((triple1) -> (rule2 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple2) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple2) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple2) -> (rule5 % int3)) ((triple2 ((triple2) -> (rule5 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3