Dave is big. Dave is white. Dave is young. Erin is nice. Erin is round. Harry is red. Harry is round. All young people are nice. Nice people are furry. All furry people are red.
Dave is big.
("Dave" "is" "big" "+")
Dave is white.
("Dave" "is" "white" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is round.
("Erin" "is" "round" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is round.
("Harry" "is" "round" "+")
All young people are nice.
((("someone" "is" "young" "+")) -> ("someone" "is" "nice" "+"))
Nice people are furry.
((("someone" "is" "nice" "+")) -> ("someone" "is" "furry" "+"))
All furry people are red.
((("someone" "is" "furry" "+")) -> ("someone" "is" "red" "+"))
Harry is round.
True
1
proof
[(triple7)]
("Harry" "is" "round" "+")
triple7
Dave is not big.
False
1
inv-proof
[(triple1)]
("Dave" "is" "big" "-")
triple1
Erin is furry.
True
2
proof
[(((triple4) -> rule2))]
("Erin" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule1))]
("Dave" "is" "nice" "-")
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is red.
True
3
proof
[(((((triple4) -> rule2)) -> rule3))]
("Erin" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is not furry.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2))]
("Dave" "is" "furry" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is furry.
Unknown
rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule2 <- rule1 <- FAIL)]]
("Harry" "is" "furry" "+")
Erin is not white.
Unknown
inv-random
[@0: Erin is white.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "white" "-")
Harry is white.
Unknown
random
[@0: Harry is white.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "white" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Erin is young.
Unknown
random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "+")
@0: Dave is big.[(triple1)] Dave is white.[(triple2)] Dave is young.[(triple3)] Erin is nice.[(triple4)] Erin is round.[(triple5)] Harry is red.[(triple6)] Harry is round.[(triple7)] @1: Dave is nice.[(((triple3) -> rule1))] Erin is furry.[(((triple4) -> rule2))] @2: Dave is furry.[(((((triple3) -> rule1)) -> rule2))] Erin is red.[(((((triple4) -> rule2)) -> rule3))] @3: Dave is red.[(((((((triple3) -> rule1)) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is white.
("Dave" "is" "white" "+")
triple2
Dave is young.
("Dave" "is" "young" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Harry is red.
("Harry" "is" "red" "+")
triple6
Harry is round.
("Harry" "is" "round" "+")
triple7
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
((triple4) -> (rule2 % int1))
Erin is furry.
("Erin" "is" "furry" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is red.
("Erin" "is" "red" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Erin is red.
("Erin" "is" "red" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((((triple3) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3