Dave is big. Dave is young. Erin is nice. Young people are round. If Dave is furry then Dave is round. All quiet people are young. Quiet people are young. If someone is big and round then they are young. Young people are quiet. All big, quiet people are furry. Furry people are smart.
Dave is big.
("Dave" "is" "big" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If Dave is furry then Dave is round.
((("Dave" "is" "furry" "+")) -> ("Dave" "is" "round" "+"))
All quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
Quiet people are young.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "young" "+"))
If someone is big and round then they are young.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "young" "+"))
Young people are quiet.
((("someone" "is" "young" "+")) -> ("someone" "is" "quiet" "+"))
All big, quiet people are furry.
((("someone" "is" "big" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "furry" "+"))
Furry people are smart.
((("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
Erin is nice.
True
1
proof
[(triple3)]
("Erin" "is" "nice" "+")
triple3
Erin is not nice.
False
1
inv-proof
[(triple3)]
("Erin" "is" "nice" "-")
triple3
Dave is quiet.
True
2
proof
[(((triple2) -> rule6))]
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is not round.
False
2
inv-proof
[(((triple2) -> rule1) OR ((((triple1 ((triple2) -> rule6)) -> rule7)) -> rule2))]
("Dave" "is" "round" "-")
((triple2) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is furry.
True
4
proof
[(((triple1 ((triple2) -> rule6)) -> rule7))]
("Dave" "is" "furry" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is not furry.
False
4
inv-proof
[(((triple1 ((triple2) -> rule6)) -> rule7))]
("Dave" "is" "furry" "-")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
True
5
proof
[(((((triple1 ((triple2) -> rule6)) -> rule7)) -> rule8))]
("Dave" "is" "smart" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is not smart.
False
5
inv-proof
[(((((triple1 ((triple2) -> rule6)) -> rule7)) -> rule8))]
("Dave" "is" "smart" "-")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Erin is not quiet.
Unknown
inv-rconc
[@2: Erin is quiet.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Erin" "is" "quiet" "-")
Erin is round.
Unknown
rconc
[@4: Erin is round.[CWA. Example of deepest failure = (rule1 <- rule3 <- rule6 <- rule4 <- FAIL)]]
("Erin" "is" "round" "+")
Erin is not young.
Unknown
inv-rconc
[@3: Erin is young.[CWA. Example of deepest failure = (rule3 <- rule6 <- rule4 <- FAIL)]]
("Erin" "is" "young" "-")
Erin is smart.
Unknown
rconc
[@2: Erin is smart.[CWA. Example of deepest failure = (rule8 <- rule7 <- FAIL)]]
("Erin" "is" "smart" "+")
Erin is not big.
Unknown
inv-random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
@0: Dave is big.[(triple1)] Dave is young.[(triple2)] Erin is nice.[(triple3)] @1: Dave is quiet.[(((triple2) -> rule6))] Dave is round.[(((triple2) -> rule1) OR ((((triple1 ((triple2) -> rule6)) -> rule7)) -> rule2))] @2: Dave is furry.[(((triple1 ((triple2) -> rule6)) -> rule7))] @3: Dave is smart.[(((((triple1 ((triple2) -> rule6)) -> rule7)) -> rule8))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is young.
("Dave" "is" "young" "+")
triple2
Erin is nice.
("Erin" "is" "nice" "+")
triple3
Dave is quiet.
("Dave" "is" "quiet" "+")
((triple2) -> (rule6 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple1 ((triple2) -> (rule6 % int2))) -> (rule7 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((triple1 ((triple2) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule8 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is quiet.
("Dave" "is" "quiet" "+")
int3