Anne is red. Erin is red. Fiona is quiet. Harry is smart. Quiet, red people are big. Quiet, smart people are young. All quiet, red people are smart. If someone is smart then they are quiet. All rough people are quiet. Rough people are red. If Erin is quiet and Erin is smart then Erin is red. All red, big people are young.
Anne is red.
("Anne" "is" "red" "+")
Erin is red.
("Erin" "is" "red" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Quiet, red people are big.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Quiet, smart people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All quiet, red people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If someone is smart then they are quiet.
((("someone" "is" "smart" "+")) -> ("someone" "is" "quiet" "+"))
All rough people are quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "+"))
Rough people are red.
((("someone" "is" "rough" "+")) -> ("someone" "is" "red" "+"))
If Erin is quiet and Erin is smart then Erin is red.
((("Erin" "is" "quiet" "+") ("Erin" "is" "smart" "+")) -> ("Erin" "is" "red" "+"))
All red, big people are young.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Harry is not smart.
False
1
inv-proof
[(triple4)]
("Harry" "is" "smart" "-")
triple4
Harry is quiet.
True
2
proof
[(((triple4) -> rule4))]
("Harry" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is not quiet.
False
2
inv-proof
[(((triple4) -> rule4))]
("Harry" "is" "quiet" "-")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
True
4
proof
[(((((triple4) -> rule4) triple4) -> rule2))]
("Harry" "is" "young" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is not young.
False
4
inv-proof
[(((((triple4) -> rule4) triple4) -> rule2))]
("Harry" "is" "young" "-")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Anne is not young.
Unknown
inv-rconc
[@5: Anne is young.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule4 <- rule3 <- rule5 <- FAIL)]]
("Anne" "is" "young" "-")
Erin is young.
Unknown
rconc
[@5: Erin is young.[CWA. Example of deepest failure = (rule8 <- rule1 <- rule4 <- rule3 <- rule5 <- FAIL)]]
("Erin" "is" "young" "+")
Erin is not quiet.
Unknown
inv-rconc
[@3: Erin is quiet.[CWA. Example of deepest failure = (rule4 <- rule3 <- rule5 <- FAIL)]]
("Erin" "is" "quiet" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is green.
Unknown
random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "+")
@0: Anne is red.[(triple1)] Erin is red.[(triple2)] Fiona is quiet.[(triple3)] Harry is smart.[(triple4)] @1: Harry is quiet.[(((triple4) -> rule4))] @2: Harry is young.[(((((triple4) -> rule4) triple4) -> rule2))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Erin is red.
("Erin" "is" "red" "+")
triple2
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple3
Harry is smart.
("Harry" "is" "smart" "+")
triple4
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
((((triple4) -> (rule4 % int2)) triple4) -> (rule2 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2