Charlie is round. Fiona is green. If someone is round then they are green. If someone is white then they are red. Green people are smart. If someone is white then they are red. Smart people are green. If Charlie is big and Charlie is nice then Charlie is green.
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is green.
("Fiona" "is" "green" "+")
If someone is round then they are green.
((("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Green people are smart.
((("someone" "is" "green" "+")) -> ("someone" "is" "smart" "+"))
If someone is white then they are red.
((("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Smart people are green.
((("someone" "is" "smart" "+")) -> ("someone" "is" "green" "+"))
If Charlie is big and Charlie is nice then Charlie is green.
((("Charlie" "is" "big" "+") ("Charlie" "is" "nice" "+")) -> ("Charlie" "is" "green" "+"))
Charlie is round.
True
1
proof
[(triple1)]
("Charlie" "is" "round" "+")
triple1
Charlie is not round.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "round" "-")
triple1
Charlie is green.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple2) -> rule3))]
("Fiona" "is" "smart" "-")
((triple2) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Charlie is smart.
True
3
proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not smart.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule3))]
("Charlie" "is" "smart" "-")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not red.
Unknown
inv-rconc
[@1: Charlie is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "red" "+")
Charlie is not nice.
Unknown
inv-random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is white.
Unknown
random
[@0: Charlie is white.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not big.
Unknown
inv-random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "-")
Fiona is big.
Unknown
random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "+")
@0: Charlie is round.[(triple1)] Fiona is green.[(triple2)] @1: Charlie is green.[(((triple1) -> rule1))] Fiona is smart.[(((triple2) -> rule3))] @2: Charlie is smart.[(((((triple1) -> rule1)) -> rule3))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
((triple1) -> (rule1 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2