Charlie is rough. Charlie is young. Erin is kind. Erin is nice. Erin is rough. Fiona is rough. Fiona is young. If something is young and nice then it is round. All kind, rough things are young. Smart, quiet things are round. If something is nice then it is quiet. All nice, round things are smart. If something is smart and nice then it is rough. If Fiona is young then Fiona is rough. Kind things are nice.
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is young.
("Fiona" "is" "young" "+")
If something is young and nice then it is round.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "round" "+"))
All kind, rough things are young.
((("something" "is" "kind" "+") ("something" "is" "rough" "+")) -> ("something" "is" "young" "+"))
Smart, quiet things are round.
((("something" "is" "smart" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "round" "+"))
If something is nice then it is quiet.
((("something" "is" "nice" "+")) -> ("something" "is" "quiet" "+"))
All nice, round things are smart.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If something is smart and nice then it is rough.
((("something" "is" "smart" "+") ("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
If Fiona is young then Fiona is rough.
((("Fiona" "is" "young" "+")) -> ("Fiona" "is" "rough" "+"))
Kind things are nice.
((("something" "is" "kind" "+")) -> ("something" "is" "nice" "+"))
Erin is rough.
True
1
proof
[(triple5)]
("Erin" "is" "rough" "+")
triple5
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Fiona is not round.
Unknown
inv-rconc
[@3: Fiona is round.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule8 <- FAIL)]]
("Fiona" "is" "round" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Charlie is rough.[(triple1)] Charlie is young.[(triple2)] Erin is kind.[(triple3)] Erin is nice.[(triple4 OR ((triple3) -> rule8))] Erin is rough.[(triple5)] Fiona is rough.[(triple6 OR ((triple7) -> rule7))] Fiona is young.[(triple7)] @1: Erin is quiet.[(((triple4) -> rule4) OR ((((triple3) -> rule8)) -> rule4))] Erin is young.[(((triple3 triple5) -> rule2))] @2: Erin is round.[(((((triple3 triple5) -> rule2) triple4) -> rule1) OR ((((triple3 triple5) -> rule2) ((triple3) -> rule8)) -> rule1))] @3: Erin is smart.[(((triple4 ((((triple3 triple5) -> rule2) triple4) -> rule1)) -> rule5) OR ((triple4 ((((triple3 triple5) -> rule2) ((triple3) -> rule8)) -> rule1)) -> rule5) OR ((((triple3) -> rule8) ((((triple3 triple5) -> rule2) triple4) -> rule1)) -> rule5) OR ((((triple3) -> rule8) ((((triple3 triple5) -> rule2) ((triple3) -> rule8)) -> rule1)) -> rule5))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
((triple3) -> (rule8 % int1))
Erin is nice.
("Erin" "is" "nice" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
triple5
Fiona is rough.
("Fiona" "is" "rough" "+")
triple6
((triple7) -> (rule7 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple7
Erin is quiet.
("Erin" "is" "quiet" "+")
((triple4) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
((((triple3) -> (rule8 % int2))) -> (rule4 % int1))
Erin is quiet.
("Erin" "is" "quiet" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
((triple3 triple5) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
((((triple3 triple5) -> (rule2 % int2)) triple4) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((((triple3 triple5) -> (rule2 % int3)) ((triple3) -> (rule8 % int2))) -> (rule1 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is nice.
("Erin" "is" "nice" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is smart.
("Erin" "is" "smart" "+")
((triple4 ((((triple3 triple5) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((triple4 ((((triple3 triple5) -> (rule2 % int4)) ((triple3) -> (rule8 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is nice.
("Erin" "is" "nice" "+")
int3
Erin is young.
("Erin" "is" "young" "+")
int4
((((triple3) -> (rule8 % int4)) ((((triple3 triple5) -> (rule2 % int3)) triple4) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4
((((triple3) -> (rule8 % int4)) ((((triple3 triple5) -> (rule2 % int3)) ((triple3) -> (rule8 % int4))) -> (rule1 % int2))) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
Erin is nice.
("Erin" "is" "nice" "+")
int4