Anne is furry. Charlie is young. Erin is big. Gary is smart. If Erin is furry and Erin is rough then Erin is big. If someone is round and young then they are kind. All smart people are rough. All big people are young. Big people are smart. If someone is big and rough then they are round. All smart, round people are big. All young people are round.
Anne is furry.
("Anne" "is" "furry" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Erin is big.
("Erin" "is" "big" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If Erin is furry and Erin is rough then Erin is big.
((("Erin" "is" "furry" "+") ("Erin" "is" "rough" "+")) -> ("Erin" "is" "big" "+"))
If someone is round and young then they are kind.
((("someone" "is" "round" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "kind" "+"))
All smart people are rough.
((("someone" "is" "smart" "+")) -> ("someone" "is" "rough" "+"))
All big people are young.
((("someone" "is" "big" "+")) -> ("someone" "is" "young" "+"))
Big people are smart.
((("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
If someone is big and rough then they are round.
((("someone" "is" "big" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "round" "+"))
All smart, round people are big.
((("someone" "is" "smart" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
Charlie is young.
True
1
proof
[(triple2)]
("Charlie" "is" "young" "+")
triple2
Erin is not big.
False
1
inv-proof
[(triple3)]
("Erin" "is" "big" "-")
triple3
Erin is young.
True
2
proof
[(((triple3) -> rule4))]
("Erin" "is" "young" "+")
((triple3) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is not rough.
False
2
inv-proof
[(((triple4) -> rule3))]
("Gary" "is" "rough" "-")
((triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is kind.
True
4
proof
[(((((triple2) -> rule8) triple2) -> rule2))]
("Charlie" "is" "kind" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Charlie is not kind.
False
4
inv-proof
[(((((triple2) -> rule8) triple2) -> rule2))]
("Charlie" "is" "kind" "-")
((((triple2) -> (rule8 % int2)) triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is kind.
True
6
proof
[(((((((triple3) -> rule4)) -> rule8) ((triple3) -> rule4)) -> rule2) OR ((((triple3 ((((triple3) -> rule5)) -> rule3)) -> rule6) ((triple3) -> rule4)) -> rule2))]
("Erin" "is" "kind" "+")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) ((triple3) -> (rule4 % int3))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Erin is not kind.
False
6
inv-proof
[(((((((triple3) -> rule4)) -> rule8) ((triple3) -> rule4)) -> rule2) OR ((((triple3 ((((triple3) -> rule5)) -> rule3)) -> rule6) ((triple3) -> rule4)) -> rule2))]
("Erin" "is" "kind" "-")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) ((triple3) -> (rule4 % int3))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5
Gary is not big.
Unknown
inv-rconc
[@3: Gary is big.[CWA. Example of deepest failure = (rule7 <- rule8 <- rule4 <- FAIL)]]
("Gary" "is" "big" "-")
Gary is kind.
Unknown
rconc
[@4: Gary is kind.[CWA. Example of deepest failure = (rule2 <- rule4 <- rule7 <- rule6 <- FAIL)]]
("Gary" "is" "kind" "+")
Anne is not young.
Unknown
inv-rconc
[@3: Anne is young.[CWA. Example of deepest failure = (rule4 <- rule7 <- rule5 <- FAIL)]]
("Anne" "is" "young" "-")
Anne is rough.
Unknown
rconc
[@3: Anne is rough.[CWA. Example of deepest failure = (rule3 <- rule5 <- rule7 <- FAIL)]]
("Anne" "is" "rough" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
@0: Anne is furry.[(triple1)] Charlie is young.[(triple2)] Erin is big.[(triple3)] Gary is smart.[(triple4)] @1: Charlie is round.[(((triple2) -> rule8))] Erin is smart.[(((triple3) -> rule5))] Erin is young.[(((triple3) -> rule4))] Gary is rough.[(((triple4) -> rule3))] @2: Charlie is kind.[(((((triple2) -> rule8) triple2) -> rule2))] Erin is rough.[(((((triple3) -> rule5)) -> rule3))] Erin is round.[(((((triple3) -> rule4)) -> rule8) OR ((triple3 ((((triple3) -> rule5)) -> rule3)) -> rule6))] @3: Erin is kind.[(((((((triple3) -> rule4)) -> rule8) ((triple3) -> rule4)) -> rule2) OR ((((triple3 ((((triple3) -> rule5)) -> rule3)) -> rule6) ((triple3) -> rule4)) -> rule2))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
((triple2) -> (rule8 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
((triple3) -> (rule5 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple3) -> (rule4 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
((triple4) -> (rule3 % int1))
Gary is rough.
("Gary" "is" "rough" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2) -> (rule8 % int2)) triple2) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is round.
("Charlie" "is" "round" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
((((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
((((triple3) -> (rule4 % int2))) -> (rule8 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule6 % int1))
Erin is round.
("Erin" "is" "round" "+")
int1
Erin is rough.
("Erin" "is" "rough" "+")
int2
Erin is smart.
("Erin" "is" "smart" "+")
int3
Erin is kind.
("Erin" "is" "kind" "+")
((((((triple3) -> (rule4 % int3))) -> (rule8 % int2)) ((triple3) -> (rule4 % int3))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is round.
("Erin" "is" "round" "+")
int2
Erin is young.
("Erin" "is" "young" "+")
int3
((((triple3 ((((triple3) -> (rule5 % int5))) -> (rule3 % int4))) -> (rule6 % int3)) ((triple3) -> (rule4 % int2))) -> (rule2 % int1))
Erin is kind.
("Erin" "is" "kind" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
int3
Erin is rough.
("Erin" "is" "rough" "+")
int4
Erin is smart.
("Erin" "is" "smart" "+")
int5