Charlie is nice. Fiona is round. Gary is white. Harry is smart. All nice, white people are furry. All smart people are round. If Fiona is quiet and Fiona is round then Fiona is white. All round people are smart. White people are smart. All quiet people are smart. Round people are not quiet. If Fiona is quiet then Fiona is not round.
Charlie is nice.
("Charlie" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Gary is white.
("Gary" "is" "white" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All nice, white people are furry.
((("someone" "is" "nice" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "furry" "+"))
All smart people are round.
((("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
If Fiona is quiet and Fiona is round then Fiona is white.
((("Fiona" "is" "quiet" "+") ("Fiona" "is" "round" "+")) -> ("Fiona" "is" "white" "+"))
All round people are smart.
((("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
White people are smart.
((("someone" "is" "white" "+")) -> ("someone" "is" "smart" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Round people are not quiet.
((("someone" "is" "round" "+")) -> ("someone" "is" "quiet" "-"))
If Fiona is quiet then Fiona is not round.
((("Fiona" "is" "quiet" "+")) -> ("Fiona" "is" "round" "-"))
Fiona is round.
True
1
proof
[(triple2)]
("Fiona" "is" "round" "+")
triple2
Fiona is not round.
False
1
inv-proof
[(triple2)]
("Fiona" "is" "round" "-")
triple2
Harry is round.
True
2
proof
[(((triple4) -> rule2))]
("Harry" "is" "round" "+")
((triple4) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple2) -> rule4))]
("Fiona" "is" "smart" "-")
((triple2) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is not quiet.
True
3
proof
[(((((triple4) -> rule2)) -> rule7))]
("Harry" "is" "quiet" "-")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is quiet.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule7))]
("Harry" "is" "quiet" "+")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is not quiet.
True
4
proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is quiet.
False
4
inv-proof
[(((((((triple3) -> rule5)) -> rule2)) -> rule7))]
("Gary" "is" "quiet" "+")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Fiona is not white.
Unknown
inv-rconc
[@1: Fiona is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "white" "-")
Fiona is furry.
Unknown
rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "furry" "-")
Charlie is smart.
Unknown
rconc
[@3: Charlie is smart.[CWA. Example of deepest failure = (rule4 <- rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Harry is blue.
Unknown
random
[@0: Harry is blue.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "blue" "+")
@0: Charlie is nice.[(triple1)] Fiona is round.[(triple2)] Gary is white.[(triple3)] Harry is smart.[(triple4)] @1: Fiona is not quiet.[(((triple2) -> rule7))] Fiona is smart.[(((triple2) -> rule4))] Gary is smart.[(((triple3) -> rule5))] Harry is round.[(((triple4) -> rule2))] @2: Gary is round.[(((((triple3) -> rule5)) -> rule2))] Harry is not quiet.[(((((triple4) -> rule2)) -> rule7))] @3: Gary is not quiet.[(((((((triple3) -> rule5)) -> rule2)) -> rule7))]
Charlie is nice.
("Charlie" "is" "nice" "+")
triple1
Fiona is round.
("Fiona" "is" "round" "+")
triple2
Gary is white.
("Gary" "is" "white" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple2) -> (rule7 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple2) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple4) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((((triple3) -> (rule5 % int2))) -> (rule2 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Harry is not quiet.
("Harry" "is" "quiet" "-")
((((triple4) -> (rule2 % int2))) -> (rule7 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Gary is not quiet.
("Gary" "is" "quiet" "-")
((((((triple3) -> (rule5 % int3))) -> (rule2 % int2))) -> (rule7 % int1))
Gary is not quiet.
("Gary" "is" "quiet" "-")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3