Anne is red. Anne is rough. Anne is not young. Charlie is green. Charlie is young. Fiona is furry. Fiona is red. If Fiona is young then Fiona is green. Furry people are not young. Rough people are not quiet. If Fiona is furry then Fiona is not quiet. If Charlie is rough and Charlie is smart then Charlie is red. If someone is rough then they are smart. If someone is young and green then they are rough. If Fiona is red and Fiona is not green then Fiona is not smart.
Anne is red.
("Anne" "is" "red" "+")
Anne is rough.
("Anne" "is" "rough" "+")
Anne is not young.
("Anne" "is" "young" "-")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is red.
("Fiona" "is" "red" "+")
If Fiona is young then Fiona is green.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "green" "+"))
Furry people are not young.
((("someone" "is" "furry" "+")) -> ("someone" "is" "young" "-"))
Rough people are not quiet.
((("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
If Fiona is furry then Fiona is not quiet.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "quiet" "-"))
If Charlie is rough and Charlie is smart then Charlie is red.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "smart" "+")) -> ("Charlie" "is" "red" "+"))
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If someone is young and green then they are rough.
((("someone" "is" "young" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is red and Fiona is not green then Fiona is not smart.
((("Fiona" "is" "red" "+") ("Fiona" "is" "green" "~")) -> ("Fiona" "is" "smart" "-"))
Anne is red.
True
1
proof
[(triple1)]
("Anne" "is" "red" "+")
triple1
Anne is young.
False
1
inv-proof
[(triple3)]
("Anne" "is" "young" "+")
triple3
Anne is smart.
True
2
proof
[(((triple2) -> rule6))]
("Anne" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is not smart.
False
2
inv-proof
[(((triple2) -> rule6))]
("Anne" "is" "smart" "-")
((triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is smart.
True
4
proof
[(((((triple5 triple4) -> rule7)) -> rule6))]
("Charlie" "is" "smart" "+")
((((triple5 triple4) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is quiet.
False
4
inv-proof
[(((((triple5 triple4) -> rule7)) -> rule3))]
("Charlie" "is" "quiet" "+")
((((triple5 triple4) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
True
8
proof
[(((((triple5 triple4) -> rule7) ((((triple5 triple4) -> rule7)) -> rule6)) -> rule5))]
("Charlie" "is" "red" "+")
((((triple5 triple4) -> (rule7 % int3)) ((((triple5 triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is not red.
False
8
inv-proof
[(((((triple5 triple4) -> rule7) ((((triple5 triple4) -> rule7)) -> rule6)) -> rule5))]
("Charlie" "is" "red" "-")
((((triple5 triple4) -> (rule7 % int3)) ((((triple5 triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Fiona is not rough.
Unknown
inv-rconc
[@1: Fiona is rough.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is green.
Unknown
rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "+")
Fiona is not smart.
Unknown
inv-rconc
[@2: Fiona is smart.[CWA. Example of deepest failure = (rule6 <- rule7 <- FAIL)]]
("Fiona" "is" "smart" "-")
Charlie is furry.
Unknown
random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "+")
Anne is not furry.
Unknown
inv-random
[@0: Anne is furry.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "furry" "-")
Anne is green.
Unknown
random
[@0: Anne is green.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "green" "+")
@0: Anne is not young.[(triple3)] Anne is red.[(triple1)] Anne is rough.[(triple2)] Charlie is green.[(triple4)] Charlie is young.[(triple5)] Fiona is furry.[(triple6)] Fiona is red.[(triple7)] @1: Anne is not quiet.[(((triple2) -> rule3))] Anne is smart.[(((triple2) -> rule6))] Charlie is rough.[(((triple5 triple4) -> rule7))] Fiona is not quiet.[(((triple6) -> rule4))] Fiona is not young.[(((triple6) -> rule2))] @2: Charlie is not quiet.[(((((triple5 triple4) -> rule7)) -> rule3))] Charlie is smart.[(((((triple5 triple4) -> rule7)) -> rule6))] @3: Charlie is red.[(((((triple5 triple4) -> rule7) ((((triple5 triple4) -> rule7)) -> rule6)) -> rule5))]
Anne is not young.
("Anne" "is" "young" "-")
triple3
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is rough.
("Anne" "is" "rough" "+")
triple2
Charlie is green.
("Charlie" "is" "green" "+")
triple4
Charlie is young.
("Charlie" "is" "young" "+")
triple5
Fiona is furry.
("Fiona" "is" "furry" "+")
triple6
Fiona is red.
("Fiona" "is" "red" "+")
triple7
Anne is not quiet.
("Anne" "is" "quiet" "-")
((triple2) -> (rule3 % int1))
Anne is not quiet.
("Anne" "is" "quiet" "-")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple5 triple4) -> (rule7 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple6) -> (rule4 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Fiona is not young.
("Fiona" "is" "young" "-")
((triple6) -> (rule2 % int1))
Fiona is not young.
("Fiona" "is" "young" "-")
int1
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
((((triple5 triple4) -> (rule7 % int2))) -> (rule3 % int1))
Charlie is not quiet.
("Charlie" "is" "quiet" "-")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
((((triple5 triple4) -> (rule7 % int2))) -> (rule6 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple5 triple4) -> (rule7 % int3)) ((((triple5 triple4) -> (rule7 % int3))) -> (rule6 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3