Anne is furry. Charlie is furry. Charlie is red. Charlie is rough. Dave is furry. Dave is young. Fiona is blue. All smart people are red. All blue, rough people are smart. Young people are nice. All nice people are rough. If someone is rough and young then they are blue. All furry, smart people are nice.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
All smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All blue, rough people are smart.
((("someone" "is" "blue" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
All nice people are rough.
((("someone" "is" "nice" "+")) -> ("someone" "is" "rough" "+"))
If someone is rough and young then they are blue.
((("someone" "is" "rough" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "blue" "+"))
All furry, smart people are nice.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Dave is furry.
True
1
proof
[(triple5)]
("Dave" "is" "furry" "+")
triple5
Charlie is not furry.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "furry" "-")
triple2
Dave is nice.
True
2
proof
[(((triple6) -> rule3))]
("Dave" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple6) -> rule3))]
("Dave" "is" "nice" "-")
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
True
3
proof
[(((((triple6) -> rule3)) -> rule4))]
("Dave" "is" "rough" "+")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is not rough.
False
3
inv-proof
[(((((triple6) -> rule3)) -> rule4))]
("Dave" "is" "rough" "-")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
True
5
proof
[(((((((triple6) -> rule3)) -> rule4) triple6) -> rule5))]
("Dave" "is" "blue" "+")
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is not blue.
False
5
inv-proof
[(((((((triple6) -> rule3)) -> rule4) triple6) -> rule5))]
("Dave" "is" "blue" "-")
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
True
9
proof
[(((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2))]
("Dave" "is" "smart" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2)) ((((triple6) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is not smart.
False
9
inv-proof
[(((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2))]
("Dave" "is" "smart" "-")
((((((((triple6) -> (rule3 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2)) ((((triple6) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is red.
True
10
proof
[(((((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2)) -> rule1))]
("Dave" "is" "red" "+")
((((((((((triple6) -> (rule3 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3)) ((((triple6) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Dave is not red.
False
10
inv-proof
[(((((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2)) -> rule1))]
("Dave" "is" "red" "-")
((((((((((triple6) -> (rule3 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3)) ((((triple6) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5
Anne is not red.
Unknown
inv-rconc
[@3: Anne is red.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule5 <- FAIL)]]
("Anne" "is" "red" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "nice" "+")
Charlie is not smart.
Unknown
inv-rconc
[@2: Charlie is smart.[CWA. Example of deepest failure = (rule2 <- rule5 <- FAIL)]]
("Charlie" "is" "smart" "-")
Anne is nice.
Unknown
rconc
[@3: Anne is nice.[CWA. Example of deepest failure = (rule6 <- rule2 <- rule5 <- FAIL)]]
("Anne" "is" "nice" "+")
Fiona is not rough.
Unknown
inv-rconc
[@2: Fiona is rough.[CWA. Example of deepest failure = (rule4 <- rule3 <- FAIL)]]
("Fiona" "is" "rough" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule4 <- rule6 <- rule2 <- FAIL)]]
("Anne" "is" "rough" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Fiona is furry.
Unknown
random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "+")
Anne is not young.
Unknown
inv-random
[@0: Anne is young.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "young" "-")
Charlie is young.
Unknown
random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "+")
@0: Anne is furry.[(triple1)] Charlie is furry.[(triple2)] Charlie is red.[(triple3)] Charlie is rough.[(triple4)] Dave is furry.[(triple5)] Dave is young.[(triple6)] Fiona is blue.[(triple7)] @1: Dave is nice.[(((triple6) -> rule3))] @2: Dave is rough.[(((((triple6) -> rule3)) -> rule4))] @3: Dave is blue.[(((((((triple6) -> rule3)) -> rule4) triple6) -> rule5))] @4: Dave is smart.[(((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2))] @5: Dave is red.[(((((((((((triple6) -> rule3)) -> rule4) triple6) -> rule5) ((((triple6) -> rule3)) -> rule4)) -> rule2)) -> rule1))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
triple5
Dave is young.
("Dave" "is" "young" "+")
triple6
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple6) -> (rule3 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
((((triple6) -> (rule3 % int2))) -> (rule4 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((((triple6) -> (rule3 % int3))) -> (rule4 % int2)) triple6) -> (rule5 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is smart.
("Dave" "is" "smart" "+")
((((((((triple6) -> (rule3 % int4))) -> (rule4 % int3)) triple6) -> (rule5 % int2)) ((((triple6) -> (rule3 % int4))) -> (rule4 % int3))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is rough.
("Dave" "is" "rough" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
int4
Dave is red.
("Dave" "is" "red" "+")
((((((((((triple6) -> (rule3 % int5))) -> (rule4 % int4)) triple6) -> (rule5 % int3)) ((((triple6) -> (rule3 % int5))) -> (rule4 % int4))) -> (rule2 % int2))) -> (rule1 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
int3
Dave is rough.
("Dave" "is" "rough" "+")
int4
Dave is nice.
("Dave" "is" "nice" "+")
int5