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