Anne is big. Anne is green. Anne is young. Erin is not smart. Erin is young. Gary is not green. Gary is not smart. Harry is big. Harry is not kind. Harry is quiet. Harry is red. Harry is not young. Quiet people are smart. Green people are quiet.
Anne is big.
("Anne" "is" "big" "+")
Anne is green.
("Anne" "is" "green" "+")
Anne is young.
("Anne" "is" "young" "+")
Erin is not smart.
("Erin" "is" "smart" "-")
Erin is young.
("Erin" "is" "young" "+")
Gary is not green.
("Gary" "is" "green" "-")
Gary is not smart.
("Gary" "is" "smart" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is not kind.
("Harry" "is" "kind" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is not young.
("Harry" "is" "young" "-")
Quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
Green people are quiet.
((("someone" "is" "green" "+")) -> ("someone" "is" "quiet" "+"))
Harry is big.
True
1
proof
[(triple8)]
("Harry" "is" "big" "+")
triple8
Anne is not young.
False
1
inv-proof
[(triple3)]
("Anne" "is" "young" "-")
triple3
Harry is smart.
True
2
proof
[(((triple10) -> rule1))]
("Harry" "is" "smart" "+")
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is not quiet.
False
2
inv-proof
[(((triple2) -> rule2))]
("Anne" "is" "quiet" "-")
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
True
3
proof
[(((((triple2) -> rule2)) -> rule1))]
("Anne" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Anne is not smart.
False
3
inv-proof
[(((((triple2) -> rule2)) -> rule1))]
("Anne" "is" "smart" "-")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2
Gary is not quiet.
Unknown
inv-rconc
[@1: Gary is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "quiet" "-")
Erin is quiet.
Unknown
rconc
[@1: Erin is quiet.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Erin" "is" "quiet" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Anne is not red.
Unknown
inv-random
[@0: Anne is red.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "red" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Anne is big.[(triple1)] Anne is green.[(triple2)] Anne is young.[(triple3)] Erin is not smart.[(triple4)] Erin is young.[(triple5)] Gary is not green.[(triple6)] Gary is not smart.[(triple7)] Harry is big.[(triple8)] Harry is not kind.[(triple9)] Harry is not young.[(triple12)] Harry is quiet.[(triple10)] Harry is red.[(triple11)] @1: Anne is quiet.[(((triple2) -> rule2))] Harry is smart.[(((triple10) -> rule1))] @2: Anne is smart.[(((((triple2) -> rule2)) -> rule1))]
Anne is big.
("Anne" "is" "big" "+")
triple1
Anne is green.
("Anne" "is" "green" "+")
triple2
Anne is young.
("Anne" "is" "young" "+")
triple3
Erin is not smart.
("Erin" "is" "smart" "-")
triple4
Erin is young.
("Erin" "is" "young" "+")
triple5
Gary is not green.
("Gary" "is" "green" "-")
triple6
Gary is not smart.
("Gary" "is" "smart" "-")
triple7
Harry is big.
("Harry" "is" "big" "+")
triple8
Harry is not kind.
("Harry" "is" "kind" "-")
triple9
Harry is not young.
("Harry" "is" "young" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple10
Harry is red.
("Harry" "is" "red" "+")
triple11
Anne is quiet.
("Anne" "is" "quiet" "+")
((triple2) -> (rule2 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple10) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((((triple2) -> (rule2 % int2))) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is quiet.
("Anne" "is" "quiet" "+")
int2