Charlie is not red. Erin is blue. Erin is not red. Erin is not round. Fiona is furry. Fiona is not red. Fiona is round. Harry is blue. Harry is smart. Harry is young. All smart things are not quiet. If something is red and not young then it is not smart. Round things are smart. All red, blue things are furry. Red, quiet things are not furry. If Fiona is blue and Fiona is smart then Fiona is quiet.
Charlie is not red.
("Charlie" "is" "red" "-")
Erin is blue.
("Erin" "is" "blue" "+")
Erin is not red.
("Erin" "is" "red" "-")
Erin is not round.
("Erin" "is" "round" "-")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is not red.
("Fiona" "is" "red" "-")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All smart things are not quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "-"))
If something is red and not young then it is not smart.
((("something" "is" "red" "+") ("something" "is" "young" "~")) -> ("something" "is" "smart" "-"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All red, blue things are furry.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Red, quiet things are not furry.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "-"))
If Fiona is blue and Fiona is smart then Fiona is quiet.
((("Fiona" "is" "blue" "+") ("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "quiet" "+"))
Erin is not red.
True
1
proof
[(triple3)]
("Erin" "is" "red" "-")
triple3
Erin is round.
False
1
inv-proof
[(triple4)]
("Erin" "is" "round" "+")
triple4
Harry is not quiet.
True
2
proof
[(((triple9) -> rule1))]
("Harry" "is" "quiet" "-")
((triple9) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple7) -> rule3))]
("Fiona" "is" "smart" "-")
((triple7) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is not quiet.
True
3
proof
[(((((triple7) -> rule3)) -> rule1))]
("Fiona" "is" "quiet" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is quiet.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule1))]
("Fiona" "is" "quiet" "+")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "furry" "-")
Erin is smart.
Unknown
rconc
[@1: Erin is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is quiet.
Unknown
random
[@0: Erin is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "quiet" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Charlie is not red.[(triple1)] Erin is blue.[(triple2)] Erin is not red.[(triple3)] Erin is not round.[(triple4)] Fiona is furry.[(triple5)] Fiona is not red.[(triple6)] Fiona is round.[(triple7)] Harry is blue.[(triple8)] Harry is smart.[(triple9)] Harry is young.[(triple10)] @1: Fiona is smart.[(((triple7) -> rule3))] Harry is not quiet.[(((triple9) -> rule1))] @2: Fiona is not quiet.[(((((triple7) -> rule3)) -> rule1))]
Charlie is not red.
("Charlie" "is" "red" "-")
triple1
Erin is blue.
("Erin" "is" "blue" "+")
triple2
Erin is not red.
("Erin" "is" "red" "-")
triple3
Erin is not round.
("Erin" "is" "round" "-")
triple4
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
Fiona is not red.
("Fiona" "is" "red" "-")
triple6
Fiona is round.
("Fiona" "is" "round" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is smart.
("Harry" "is" "smart" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple7) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is not quiet.
("Harry" "is" "quiet" "-")
((triple9) -> (rule1 % int1))
Harry is not quiet.
("Harry" "is" "quiet" "-")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((((triple7) -> (rule3 % int2))) -> (rule1 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2