Anne is blue. Charlie is big. Fiona is round. Gary is not big. If Anne is rough then Anne is not round. If someone is rough and not round then they are quiet. If Charlie is quiet then Charlie is big. If someone is blue then they are smart. If someone is smart and furry then they are blue. If someone is smart and not quiet then they are blue. All big people are blue. If someone is blue and not quiet then they are not furry.
Anne is blue.
("Anne" "is" "blue" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is not big.
("Gary" "is" "big" "-")
If Anne is rough then Anne is not round.
((("Anne" "is" "rough" "+")) -> ("Anne" "is" "round" "-"))
If someone is rough and not round then they are quiet.
((("someone" "is" "rough" "+") ("someone" "is" "round" "~")) -> ("someone" "is" "quiet" "+"))
If Charlie is quiet then Charlie is big.
((("Charlie" "is" "quiet" "+")) -> ("Charlie" "is" "big" "+"))
If someone is blue then they are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart and furry then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is smart and not quiet then they are blue.
((("someone" "is" "smart" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "blue" "+"))
All big people are blue.
((("someone" "is" "big" "+")) -> ("someone" "is" "blue" "+"))
If someone is blue and not quiet then they are not furry.
((("someone" "is" "blue" "+") ("someone" "is" "quiet" "~")) -> ("someone" "is" "furry" "-"))
Gary is not big.
True
1
proof
[(triple4)]
("Gary" "is" "big" "-")
triple4
Charlie is not big.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "big" "-")
triple2
Anne is smart.
True
2
proof
[(((triple1) -> rule4))]
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple1) -> rule4))]
("Anne" "is" "smart" "-")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Fiona is not blue.
Unknown
inv-rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "blue" "-")
Anne is quiet.
Unknown
rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Anne" "is" "quiet" "+")
Anne is not big.
Unknown
inv-random
[@0: Anne is big.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "big" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Anne is blue.[(triple1)] Charlie is big.[(triple2)] Fiona is round.[(triple3)] Gary is not big.[(triple4)] @1: Anne is smart.[(((triple1) -> rule4))] Charlie is blue.[(((triple2) -> rule7))] @2: Charlie is smart.[(((((triple2) -> rule7)) -> rule4))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Charlie is big.
("Charlie" "is" "big" "+")
triple2
Fiona is round.
("Fiona" "is" "round" "+")
triple3
Gary is not big.
("Gary" "is" "big" "-")
triple4
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule4 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple2) -> (rule7 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple2) -> (rule7 % int2))) -> (rule4 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2