Dave is big. Dave is furry. Dave is smart. Dave is young. Fiona is furry. Fiona is young. Gary is furry. All young things are furry. If Gary is smart and Gary is furry then Gary is red. Smart things are young. All big things are blue. All red, blue things are quiet. Red, quiet things are furry. All blue, big things are quiet. All big, blue things are furry.
Dave is big.
("Dave" "is" "big" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is young.
("Dave" "is" "young" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Gary is furry.
("Gary" "is" "furry" "+")
All young things are furry.
((("something" "is" "young" "+")) -> ("something" "is" "furry" "+"))
If Gary is smart and Gary is furry then Gary is red.
((("Gary" "is" "smart" "+") ("Gary" "is" "furry" "+")) -> ("Gary" "is" "red" "+"))
Smart things are young.
((("something" "is" "smart" "+")) -> ("something" "is" "young" "+"))
All big things are blue.
((("something" "is" "big" "+")) -> ("something" "is" "blue" "+"))
All red, blue things are quiet.
((("something" "is" "red" "+") ("something" "is" "blue" "+")) -> ("something" "is" "quiet" "+"))
Red, quiet things are furry.
((("something" "is" "red" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "furry" "+"))
All blue, big things are quiet.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "quiet" "+"))
All big, blue things are furry.
((("something" "is" "big" "+") ("something" "is" "blue" "+")) -> ("something" "is" "furry" "+"))
Dave is smart.
True
1
proof
[(triple3)]
("Dave" "is" "smart" "+")
triple3
Gary is not furry.
False
1
inv-proof
[(triple7)]
("Gary" "is" "furry" "-")
triple7
Dave is blue.
True
2
proof
[(((triple1) -> rule4))]
("Dave" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is not blue.
False
2
inv-proof
[(((triple1) -> rule4))]
("Dave" "is" "blue" "-")
((triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule7))]
("Dave" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is not quiet.
False
4
inv-proof
[(((((triple1) -> rule4) triple1) -> rule7))]
("Dave" "is" "quiet" "-")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Gary is not blue.
Unknown
inv-rconc
[@1: Gary is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Gary" "is" "blue" "-")
Fiona is blue.
Unknown
rconc
[@1: Fiona is blue.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Fiona" "is" "blue" "+")
Gary is not red.
Unknown
inv-rconc
[@1: Gary is red.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "red" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
Gary is not big.
Unknown
inv-random
[@0: Gary is big.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "big" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
@0: Dave is big.[(triple1)] Dave is furry.[(triple2 OR ((triple4) -> rule1) OR ((((triple3) -> rule3)) -> rule1) OR ((triple1 ((triple1) -> rule4)) -> rule8))] Dave is smart.[(triple3)] Dave is young.[(triple4 OR ((triple3) -> rule3))] Fiona is furry.[(triple5 OR ((triple6) -> rule1))] Fiona is young.[(triple6)] Gary is furry.[(triple7)] @1: Dave is blue.[(((triple1) -> rule4))] @2: Dave is quiet.[(((((triple1) -> rule4) triple1) -> rule7))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is furry.
("Dave" "is" "furry" "+")
triple2
((triple4) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
((((triple3) -> (rule3 % int2))) -> (rule1 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is young.
("Dave" "is" "young" "+")
int2
((triple1 ((triple1) -> (rule4 % int2))) -> (rule8 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Dave is young.
("Dave" "is" "young" "+")
triple4
((triple3) -> (rule3 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Fiona is furry.
("Fiona" "is" "furry" "+")
triple5
((triple6) -> (rule1 % int1))
Fiona is furry.
("Fiona" "is" "furry" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple6
Gary is furry.
("Gary" "is" "furry" "+")
triple7
Dave is blue.
("Dave" "is" "blue" "+")
((triple1) -> (rule4 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule7 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is blue.
("Dave" "is" "blue" "+")
int2