Charlie is rough. Fiona is green. Fiona is not kind. Fiona is rough. Harry is kind. Harry is quiet. Harry is rough. If something is red and furry then it is green. All big things are furry. All red things are furry. All rough, quiet things are big. If something is quiet and rough then it is red. If something is rough and not red then it is kind.
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is not kind.
("Fiona" "is" "kind" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If something is red and furry then it is green.
((("something" "is" "red" "+") ("something" "is" "furry" "+")) -> ("something" "is" "green" "+"))
All big things are furry.
((("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All red things are furry.
((("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All rough, quiet things are big.
((("something" "is" "rough" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is quiet and rough then it is red.
((("something" "is" "quiet" "+") ("something" "is" "rough" "+")) -> ("something" "is" "red" "+"))
If something is rough and not red then it is kind.
((("something" "is" "rough" "+") ("something" "is" "red" "~")) -> ("something" "is" "kind" "+"))
Charlie is rough.
True
1
proof
[(triple1)]
("Charlie" "is" "rough" "+")
triple1
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Harry is red.
True
3
proof
[(((triple6 triple7) -> rule5))]
("Harry" "is" "red" "+")
((triple6 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is not red.
False
3
inv-proof
[(((triple6 triple7) -> rule5))]
("Harry" "is" "red" "-")
((triple6 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
True
4
proof
[(((((triple6 triple7) -> rule5)) -> rule3) OR ((((triple7 triple6) -> rule4)) -> rule2))]
("Harry" "is" "furry" "+")
((((triple6 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((((triple6 triple7) -> rule5)) -> rule3) OR ((((triple7 triple6) -> rule4)) -> rule2))]
("Harry" "is" "furry" "-")
((((triple6 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
True
8
proof
[(((((triple6 triple7) -> rule5) ((((triple6 triple7) -> rule5)) -> rule3)) -> rule1) OR ((((triple6 triple7) -> rule5) ((((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "green" "+")
((((triple6 triple7) -> (rule5 % int3)) ((((triple6 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple6 triple7) -> (rule5 % int4)) ((((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Harry is not green.
False
8
inv-proof
[(((((triple6 triple7) -> rule5) ((((triple6 triple7) -> rule5)) -> rule3)) -> rule1) OR ((((triple6 triple7) -> rule5) ((((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
("Harry" "is" "green" "-")
((((triple6 triple7) -> (rule5 % int3)) ((((triple6 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple6 triple7) -> (rule5 % int4)) ((((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "big" "-")
Charlie is big.
Unknown
rconc
[@1: Charlie is big.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "big" "+")
Fiona is not furry.
Unknown
inv-rconc
[@2: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Fiona" "is" "furry" "-")
Charlie is furry.
Unknown
rconc
[@2: Charlie is furry.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Charlie" "is" "furry" "+")
Charlie is not quiet.
Unknown
inv-random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is rough.[(triple1)] Fiona is green.[(triple2)] Fiona is not kind.[(triple3)] Fiona is rough.[(triple4)] Harry is kind.[(triple5)] Harry is quiet.[(triple6)] Harry is rough.[(triple7)] @1: Harry is big.[(((triple7 triple6) -> rule4))] Harry is red.[(((triple6 triple7) -> rule5))] @2: Harry is furry.[(((((triple6 triple7) -> rule5)) -> rule3) OR ((((triple7 triple6) -> rule4)) -> rule2))] @3: Harry is green.[(((((triple6 triple7) -> rule5) ((((triple6 triple7) -> rule5)) -> rule3)) -> rule1) OR ((((triple6 triple7) -> rule5) ((((triple7 triple6) -> rule4)) -> rule2)) -> rule1))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Fiona is green.
("Fiona" "is" "green" "+")
triple2
Fiona is not kind.
("Fiona" "is" "kind" "-")
triple3
Fiona is rough.
("Fiona" "is" "rough" "+")
triple4
Harry is kind.
("Harry" "is" "kind" "+")
triple5
Harry is quiet.
("Harry" "is" "quiet" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
((triple7 triple6) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple6 triple7) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((((triple6 triple7) -> (rule5 % int2))) -> (rule3 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
((((triple7 triple6) -> (rule4 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple6 triple7) -> (rule5 % int3)) ((((triple6 triple7) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
((((triple6 triple7) -> (rule5 % int4)) ((((triple7 triple6) -> (rule4 % int3))) -> (rule2 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is red.
("Harry" "is" "red" "+")
int4