Dave is big. Dave is blue. Dave is furry. Dave is rough. Dave is smart. Fiona is blue. Fiona is quiet. Gary is not big. Gary is not blue. Gary is furry. Gary is quiet. Gary is rough. Gary is smart. Harry is big. Harry is quiet. Harry is rough. If Dave is big and Dave is quiet then Dave is furry. Rough things are furry. All furry things are kind.
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Gary is not big.
("Gary" "is" "big" "-")
Gary is not blue.
("Gary" "is" "blue" "-")
Gary is furry.
("Gary" "is" "furry" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If Dave is big and Dave is quiet then Dave is furry.
((("Dave" "is" "big" "+") ("Dave" "is" "quiet" "+")) -> ("Dave" "is" "furry" "+"))
Rough things are furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
All furry things are kind.
((("something" "is" "furry" "+")) -> ("something" "is" "kind" "+"))
Dave is furry.
True
1
proof
[(triple3 OR ((triple4) -> rule2))]
("Dave" "is" "furry" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Fiona is not quiet.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "quiet" "-")
triple7
Harry is furry.
True
2
proof
[(((triple16) -> rule2))]
("Harry" "is" "furry" "+")
((triple16) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is not furry.
False
2
inv-proof
[(((triple16) -> rule2))]
("Harry" "is" "furry" "-")
((triple16) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
True
3
proof
[(((((triple16) -> rule2)) -> rule3))]
("Harry" "is" "kind" "+")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is not kind.
False
3
inv-proof
[(((((triple16) -> rule2)) -> rule3))]
("Harry" "is" "kind" "-")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Fiona is not furry.
Unknown
inv-rconc
[@1: Fiona is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "furry" "-")
Fiona is kind.
Unknown
rconc
[@2: Fiona is kind.[CWA. Example of deepest failure = (rule3 <- rule2 <- FAIL)]]
("Fiona" "is" "kind" "+")
Fiona is not big.
Unknown
inv-random
[@0: Fiona is big.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "big" "-")
Fiona is rough.
Unknown
random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "+")
Fiona is not smart.
Unknown
inv-random
[@0: Fiona is smart.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "smart" "-")
Harry is smart.
Unknown
random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "+")
@0: Dave is big.[(triple1)] Dave is blue.[(triple2)] Dave is furry.[(triple3 OR ((triple4) -> rule2))] Dave is rough.[(triple4)] Dave is smart.[(triple5)] Fiona is blue.[(triple6)] Fiona is quiet.[(triple7)] Gary is furry.[(triple10 OR ((triple12) -> rule2))] Gary is not big.[(triple8)] Gary is not blue.[(triple9)] Gary is quiet.[(triple11)] Gary is rough.[(triple12)] Gary is smart.[(triple13)] Harry is big.[(triple14)] Harry is quiet.[(triple15)] Harry is rough.[(triple16)] @1: Dave is kind.[(((triple3) -> rule3) OR ((((triple4) -> rule2)) -> rule3))] Gary is kind.[(((triple10) -> rule3) OR ((((triple12) -> rule2)) -> rule3))] Harry is furry.[(((triple16) -> rule2))] @2: Harry is kind.[(((((triple16) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is blue.
("Dave" "is" "blue" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
((triple4) -> (rule2 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is rough.
("Dave" "is" "rough" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Gary is furry.
("Gary" "is" "furry" "+")
triple10
((triple12) -> (rule2 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is not big.
("Gary" "is" "big" "-")
triple8
Gary is not blue.
("Gary" "is" "blue" "-")
triple9
Gary is quiet.
("Gary" "is" "quiet" "+")
triple11
Gary is rough.
("Gary" "is" "rough" "+")
triple12
Gary is smart.
("Gary" "is" "smart" "+")
triple13
Harry is big.
("Harry" "is" "big" "+")
triple14
Harry is quiet.
("Harry" "is" "quiet" "+")
triple15
Harry is rough.
("Harry" "is" "rough" "+")
triple16
Dave is kind.
("Dave" "is" "kind" "+")
((triple3) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Gary is kind.
("Gary" "is" "kind" "+")
((triple10) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
((((triple12) -> (rule2 % int2))) -> (rule3 % int1))
Gary is kind.
("Gary" "is" "kind" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((triple16) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
((((triple16) -> (rule2 % int2))) -> (rule3 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2