Dave is furry. Dave is not red. Dave is round. Dave is smart. Dave is young. Erin is furry. Erin is not nice. Erin is not round. Erin is not smart. Fiona is nice. Gary is smart. Gary is white. Furry, nice things are young. If something is furry then it is young. Red things are young. If Fiona is furry then Fiona is round. All young, nice things are smart. If something is red then it is white. Round things are nice. If Gary is young and Gary is not furry then Gary is nice.
Dave is furry.
("Dave" "is" "furry" "+")
Dave is not red.
("Dave" "is" "red" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is not nice.
("Erin" "is" "nice" "-")
Erin is not round.
("Erin" "is" "round" "-")
Erin is not smart.
("Erin" "is" "smart" "-")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is white.
("Gary" "is" "white" "+")
Furry, nice things are young.
((("something" "is" "furry" "+") ("something" "is" "nice" "+")) -> ("something" "is" "young" "+"))
If something is furry then it is young.
((("something" "is" "furry" "+")) -> ("something" "is" "young" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Fiona is furry then Fiona is round.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "round" "+"))
All young, nice things are smart.
((("something" "is" "young" "+") ("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
If something is red then it is white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
Round things are nice.
((("something" "is" "round" "+")) -> ("something" "is" "nice" "+"))
If Gary is young and Gary is not furry then Gary is nice.
((("Gary" "is" "young" "+") ("Gary" "is" "furry" "~")) -> ("Gary" "is" "nice" "+"))
Erin is furry.
True
1
proof
[(triple6)]
("Erin" "is" "furry" "+")
triple6
Fiona is not nice.
False
1
inv-proof
[(triple10)]
("Fiona" "is" "nice" "-")
triple10
Dave is nice.
True
2
proof
[(((triple3) -> rule7))]
("Dave" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple3) -> rule7))]
("Dave" "is" "nice" "-")
((triple3) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Erin" "is" "white" "-")
Fiona is round.
Unknown
rconc
[@1: Fiona is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "round" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
@0: Dave is furry.[(triple1)] Dave is not red.[(triple2)] Dave is round.[(triple3)] Dave is smart.[(triple4 OR ((triple5 ((triple3) -> rule7)) -> rule5) OR ((((triple1) -> rule2) ((triple3) -> rule7)) -> rule5) OR ((((triple1 ((triple3) -> rule7)) -> rule1) ((triple3) -> rule7)) -> rule5))] Dave is young.[(triple5 OR ((triple1) -> rule2) OR ((triple1 ((triple3) -> rule7)) -> rule1))] Erin is furry.[(triple6)] Erin is not nice.[(triple7)] Erin is not round.[(triple8)] Erin is not smart.[(triple9)] Fiona is nice.[(triple10)] Gary is smart.[(triple11)] Gary is white.[(triple12)] @1: Dave is nice.[(((triple3) -> rule7))] Erin is young.[(((triple6) -> rule2))]
Dave is furry.
("Dave" "is" "furry" "+")
triple1
Dave is not red.
("Dave" "is" "red" "-")
triple2
Dave is round.
("Dave" "is" "round" "+")
triple3
Dave is smart.
("Dave" "is" "smart" "+")
triple4
((triple5 ((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
((((triple1) -> (rule2 % int3)) ((triple3) -> (rule7 % int2))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
int3
((((triple1 ((triple3) -> (rule7 % int3))) -> (rule1 % int2)) ((triple3) -> (rule7 % int3))) -> (rule5 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
Dave is nice.
("Dave" "is" "nice" "+")
int3
Dave is young.
("Dave" "is" "young" "+")
triple5
((triple1) -> (rule2 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple1 ((triple3) -> (rule7 % int2))) -> (rule1 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Erin is furry.
("Erin" "is" "furry" "+")
triple6
Erin is not nice.
("Erin" "is" "nice" "-")
triple7
Erin is not round.
("Erin" "is" "round" "-")
triple8
Erin is not smart.
("Erin" "is" "smart" "-")
triple9
Fiona is nice.
("Fiona" "is" "nice" "+")
triple10
Gary is smart.
("Gary" "is" "smart" "+")
triple11
Gary is white.
("Gary" "is" "white" "+")
triple12
Dave is nice.
("Dave" "is" "nice" "+")
((triple3) -> (rule7 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Erin is young.
("Erin" "is" "young" "+")
((triple6) -> (rule2 % int1))
Erin is young.
("Erin" "is" "young" "+")
int1