Anne is young. Dave is young. Fiona is kind. Harry is not smart. If Anne is round then Anne is rough. Kind, round people are nice. If someone is smart then they are nice. Rough, blue people are kind. All young, round people are kind. If Harry is rough then Harry is not young. If someone is young then they are round. All nice, young people are round.
Anne is young.
("Anne" "is" "young" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is kind.
("Fiona" "is" "kind" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Anne is round then Anne is rough.
((("Anne" "is" "round" "+")) -> ("Anne" "is" "rough" "+"))
Kind, round people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If someone is smart then they are nice.
((("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
Rough, blue people are kind.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young, round people are kind.
((("someone" "is" "young" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "kind" "+"))
If Harry is rough then Harry is not young.
((("Harry" "is" "rough" "+")) -> ("Harry" "is" "young" "-"))
If someone is young then they are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
All nice, young people are round.
((("someone" "is" "nice" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Harry is not smart.
True
1
proof
[(triple4)]
("Harry" "is" "smart" "-")
triple4
Anne is not young.
False
1
inv-proof
[(triple1)]
("Anne" "is" "young" "-")
triple1
Anne is round.
True
2
proof
[(((triple1) -> rule7))]
("Anne" "is" "round" "+")
((triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is not round.
False
2
inv-proof
[(((triple1) -> rule7))]
("Anne" "is" "round" "-")
((triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is kind.
True
4
proof
[(((triple2 ((triple2) -> rule7)) -> rule5))]
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule7)) -> rule5))]
("Anne" "is" "kind" "-")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is nice.
True
7
proof
[(((((triple1 ((triple1) -> rule7)) -> rule5) ((triple1) -> rule7)) -> rule2))]
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule5 % int2)) ((triple1) -> (rule7 % int3))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is not nice.
False
7
inv-proof
[(((((triple2 ((triple2) -> rule7)) -> rule5) ((triple2) -> rule7)) -> rule2))]
("Dave" "is" "nice" "-")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule7 % int3))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3
Fiona is not round.
Unknown
inv-rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "round" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "+")
Fiona is not nice.
Unknown
inv-rconc
[@2: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- rule7 <- FAIL)]]
("Fiona" "is" "nice" "-")
Harry is nice.
Unknown
rconc
[@2: Harry is nice.[CWA. Example of deepest failure = (rule2 <- rule4 <- FAIL)]]
("Harry" "is" "nice" "+")
Fiona is not young.
Unknown
inv-random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "-")
Dave is blue.
Unknown
random
[@0: Dave is blue.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "blue" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
@0: Anne is young.[(triple1)] Dave is young.[(triple2)] Fiona is kind.[(triple3)] Harry is not smart.[(triple4)] @1: Anne is round.[(((triple1) -> rule7))] Dave is round.[(((triple2) -> rule7))] @2: Anne is kind.[(((triple1 ((triple1) -> rule7)) -> rule5))] Anne is rough.[(((((triple1) -> rule7)) -> rule1))] Dave is kind.[(((triple2 ((triple2) -> rule7)) -> rule5))] @3: Anne is nice.[(((((triple1 ((triple1) -> rule7)) -> rule5) ((triple1) -> rule7)) -> rule2))] Dave is nice.[(((((triple2 ((triple2) -> rule7)) -> rule5) ((triple2) -> rule7)) -> rule2))]
Anne is young.
("Anne" "is" "young" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Fiona is kind.
("Fiona" "is" "kind" "+")
triple3
Harry is not smart.
("Harry" "is" "smart" "-")
triple4
Anne is round.
("Anne" "is" "round" "+")
((triple1) -> (rule7 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule7 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 ((triple1) -> (rule7 % int2))) -> (rule5 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is rough.
("Anne" "is" "rough" "+")
((((triple1) -> (rule7 % int2))) -> (rule1 % int1))
Anne is rough.
("Anne" "is" "rough" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Dave is kind.
("Dave" "is" "kind" "+")
((triple2 ((triple2) -> (rule7 % int2))) -> (rule5 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is nice.
("Anne" "is" "nice" "+")
((((triple1 ((triple1) -> (rule7 % int3))) -> (rule5 % int2)) ((triple1) -> (rule7 % int3))) -> (rule2 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Dave is nice.
("Dave" "is" "nice" "+")
((((triple2 ((triple2) -> (rule7 % int3))) -> (rule5 % int2)) ((triple2) -> (rule7 % int3))) -> (rule2 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
int3