Anne is green. Anne is not rough. Anne is not young. Dave is nice. Fiona is not nice. Fiona is red. Harry is big. Harry is nice. Harry is red. Harry is rough. All nice people are green. Rough people are nice. If someone is green then they are red. Nice people are quiet. All quiet people are big. If someone is big and not green then they are young. Green, quiet people are young. If Anne is rough and Anne is not nice then Anne is not red.
Anne is green.
("Anne" "is" "green" "+")
Anne is not rough.
("Anne" "is" "rough" "-")
Anne is not young.
("Anne" "is" "young" "-")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is not nice.
("Fiona" "is" "nice" "-")
Fiona is red.
("Fiona" "is" "red" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
All nice people are green.
((("someone" "is" "nice" "+")) -> ("someone" "is" "green" "+"))
Rough people are nice.
((("someone" "is" "rough" "+")) -> ("someone" "is" "nice" "+"))
If someone is green then they are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Nice people are quiet.
((("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
If someone is big and not green then they are young.
((("someone" "is" "big" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "young" "+"))
Green, quiet people are young.
((("someone" "is" "green" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If Anne is rough and Anne is not nice then Anne is not red.
((("Anne" "is" "rough" "+") ("Anne" "is" "nice" "~")) -> ("Anne" "is" "red" "-"))
Dave is nice.
True
1
proof
[(triple4)]
("Dave" "is" "nice" "+")
triple4
Harry is not rough.
False
1
inv-proof
[(triple10)]
("Harry" "is" "rough" "-")
triple10
Anne is red.
True
2
proof
[(((triple1) -> rule3))]
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1))]
("Harry" "is" "green" "-")
((triple8) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is red.
True
3
proof
[(((((triple4) -> rule1)) -> rule3))]
("Dave" "is" "red" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple4) -> rule4)) -> rule5))]
("Dave" "is" "big" "-")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Anne is not big.
Unknown
inv-rconc
[@3: Anne is big.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("Anne" "is" "big" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "young" "+")
Anne is not quiet.
Unknown
inv-rconc
[@2: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Anne" "is" "quiet" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Anne is green.[(triple1)] Anne is not rough.[(triple2)] Anne is not young.[(triple3)] Dave is nice.[(triple4)] Fiona is not nice.[(triple5)] Fiona is red.[(triple6)] Harry is big.[(triple7 OR ((((triple8) -> rule4)) -> rule5) OR ((((((triple10) -> rule2)) -> rule4)) -> rule5))] Harry is nice.[(triple8 OR ((triple10) -> rule2))] Harry is red.[(triple9 OR ((((triple8) -> rule1)) -> rule3) OR ((((((triple10) -> rule2)) -> rule1)) -> rule3))] Harry is rough.[(triple10)] @1: Anne is red.[(((triple1) -> rule3))] Dave is green.[(((triple4) -> rule1))] Dave is quiet.[(((triple4) -> rule4))] Harry is green.[(((triple8) -> rule1) OR ((((triple10) -> rule2)) -> rule1))] Harry is quiet.[(((triple8) -> rule4) OR ((((triple10) -> rule2)) -> rule4))] @2: Dave is big.[(((((triple4) -> rule4)) -> rule5))] Dave is red.[(((((triple4) -> rule1)) -> rule3))] Dave is young.[(((((triple4) -> rule1) ((triple4) -> rule4)) -> rule7))] Harry is young.[(((((triple8) -> rule1) ((triple8) -> rule4)) -> rule7) OR ((((triple8) -> rule1) ((((triple10) -> rule2)) -> rule4)) -> rule7) OR ((((((triple10) -> rule2)) -> rule1) ((triple8) -> rule4)) -> rule7) OR ((((((triple10) -> rule2)) -> rule1) ((((triple10) -> rule2)) -> rule4)) -> rule7))]
Anne is green.
("Anne" "is" "green" "+")
triple1
Anne is not rough.
("Anne" "is" "rough" "-")
triple2
Anne is not young.
("Anne" "is" "young" "-")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Fiona is not nice.
("Fiona" "is" "nice" "-")
triple5
Fiona is red.
("Fiona" "is" "red" "+")
triple6
Harry is big.
("Harry" "is" "big" "+")
triple7
((((triple8) -> (rule4 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple10) -> (rule2 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
triple9
((((triple8) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((((((triple10) -> (rule2 % int3))) -> (rule1 % int2))) -> (rule3 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is rough.
("Harry" "is" "rough" "+")
triple10
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule3 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
((triple4) -> (rule1 % int1))
Dave is green.
("Dave" "is" "green" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
((triple8) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is quiet.
("Harry" "is" "quiet" "+")
((triple8) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
((((triple10) -> (rule2 % int2))) -> (rule4 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
((((triple4) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple4) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is green.
("Dave" "is" "green" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((((triple4) -> (rule1 % int3)) ((triple4) -> (rule4 % int2))) -> (rule7 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is green.
("Dave" "is" "green" "+")
int3
Harry is young.
("Harry" "is" "young" "+")
((((triple8) -> (rule1 % int3)) ((triple8) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
((((triple8) -> (rule1 % int4)) ((((triple10) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
int4
((((((triple10) -> (rule2 % int4))) -> (rule1 % int3)) ((triple8) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4
((((((triple10) -> (rule2 % int4))) -> (rule1 % int3)) ((((triple10) -> (rule2 % int4))) -> (rule4 % int2))) -> (rule7 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Harry is quiet.
("Harry" "is" "quiet" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Harry is nice.
("Harry" "is" "nice" "+")
int4