Bob is kind. Bob is nice. Bob is red. Erin is quiet. Fiona is green. Harry is nice. Harry is red. If someone is nice and young then they are smart. If someone is quiet then they are young. If someone is young then they are nice. If someone is red and green then they are kind. If someone is green and quiet then they are red. Quiet, nice people are green.
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
If someone is nice and young then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If someone is quiet then they are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is young then they are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
If someone is red and green then they are kind.
((("someone" "is" "red" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "kind" "+"))
If someone is green and quiet then they are red.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "red" "+"))
Quiet, nice people are green.
((("someone" "is" "quiet" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Bob is kind.
True
1
proof
[(triple1)]
("Bob" "is" "kind" "+")
triple1
Erin is not quiet.
False
1
inv-proof
[(triple4)]
("Erin" "is" "quiet" "-")
triple4
Erin is young.
True
2
proof
[(((triple4) -> rule2))]
("Erin" "is" "young" "+")
((triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is not young.
False
2
inv-proof
[(((triple4) -> rule2))]
("Erin" "is" "young" "-")
((triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "nice" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is not nice.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "nice" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is smart.
True
6
proof
[(((((((triple4) -> rule2)) -> rule3) ((triple4) -> rule2)) -> rule1))]
("Erin" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) ((triple4) -> (rule2 % int3))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is not green.
False
5
inv-proof
[(((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6))]
("Erin" "is" "green" "-")
((triple4 ((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
True
7
proof
[(((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5))]
("Erin" "is" "red" "+")
((((triple4 ((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is not red.
False
7
inv-proof
[(((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5))]
("Erin" "is" "red" "-")
((((triple4 ((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is kind.
True
13
proof
[(((((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5) ((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6)) -> rule4))]
("Erin" "is" "kind" "+")
((((((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule5 % int2)) ((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Erin is not kind.
False
13
inv-proof
[(((((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5) ((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6)) -> rule4))]
("Erin" "is" "kind" "-")
((((((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule5 % int2)) ((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5
Harry is not smart.
Unknown
inv-rconc
[@2: Harry is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Harry" "is" "smart" "-")
Fiona is smart.
Unknown
rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Fiona" "is" "smart" "+")
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule4 <- rule5 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not red.
Unknown
inv-rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "red" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "green" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is kind.[(triple1)] Bob is nice.[(triple2)] Bob is red.[(triple3)] Erin is quiet.[(triple4)] Fiona is green.[(triple5)] Harry is nice.[(triple6)] Harry is red.[(triple7)] @1: Erin is young.[(((triple4) -> rule2))] @2: Erin is nice.[(((((triple4) -> rule2)) -> rule3))] @3: Erin is green.[(((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6))] Erin is smart.[(((((((triple4) -> rule2)) -> rule3) ((triple4) -> rule2)) -> rule1))] @4: Erin is red.[(((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5))] @5: Erin is kind.[(((((((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6) triple4) -> rule5) ((triple4 ((((triple4) -> rule2)) -> rule3)) -> rule6)) -> rule4))]
Bob is kind.
("Bob" "is" "kind" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Bob is red.
("Bob" "is" "red" "+")
triple3
Erin is quiet.
("Erin" "is" "quiet" "+")
triple4
Fiona is green.
("Fiona" "is" "green" "+")
triple5
Harry is nice.
("Harry" "is" "nice" "+")
triple6
Harry is red.
("Harry" "is" "red" "+")
triple7
Erin is young.
("Erin" "is" "young" "+")
((triple4) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple4 ((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2)) ((triple4) -> (rule2 % int3))) -> (rule1 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is red.
("Erin" "is" "red" "+")
((((triple4 ((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule6 % int2)) triple4) -> (rule5 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) triple4) -> (rule5 % int2)) ((triple4 ((((triple4) -> (rule2 % int5))) -> (rule3 % int4))) -> (rule6 % int3))) -> (rule4 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is red.
("Erin" "is" "red" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
Erin is young.
("Erin" "is" "young" "+")
int5