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