Charlie is not furry. Charlie is rough. Dave is furry. Dave is nice. Dave is rough. Harry is blue. Harry is rough. If someone is smart then they are blue. If someone is rough and not furry then they are smart. If someone is smart and not furry then they are rough. Big, round people are rough. If someone is furry then they are rough. If someone is round and blue then they are not nice. Blue, smart people are not round. Furry, smart people are round.
Charlie is not furry.
("Charlie" "is" "furry" "-")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Dave is rough.
("Dave" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is smart then they are blue.
((("someone" "is" "smart" "+")) -> ("someone" "is" "blue" "+"))
If someone is rough and not furry then they are smart.
((("someone" "is" "rough" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "smart" "+"))
If someone is smart and not furry then they are rough.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "~")) -> ("someone" "is" "rough" "+"))
Big, round people are rough.
((("someone" "is" "big" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
If someone is furry then they are rough.
((("someone" "is" "furry" "+")) -> ("someone" "is" "rough" "+"))
If someone is round and blue then they are not nice.
((("someone" "is" "round" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "nice" "-"))
Blue, smart people are not round.
((("someone" "is" "blue" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "-"))
Furry, smart people are round.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Charlie is rough.
True
1
proof
[(triple2)]
("Charlie" "is" "rough" "+")
triple2
Dave is not furry.
False
1
inv-proof
[(triple3)]
("Dave" "is" "furry" "-")
triple3
Charlie is smart.
True
3
proof
[(((triple2 triple1) -> rule2))]
("Charlie" "is" "smart" "+")
((triple2 triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
3
inv-proof
[(((triple2 triple1) -> rule2))]
("Charlie" "is" "smart" "-")
((triple2 triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
True
4
proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("Charlie" "is" "blue" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not blue.
False
4
inv-proof
[(((((triple2 triple1) -> rule2)) -> rule1))]
("Charlie" "is" "blue" "-")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not round.
True
8
proof
[(((((((triple2 triple1) -> rule2)) -> rule1) ((triple2 triple1) -> rule2)) -> rule7))]
("Charlie" "is" "round" "-")
((((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is round.
False
8
inv-proof
[(((((((triple2 triple1) -> rule2)) -> rule1) ((triple2 triple1) -> rule2)) -> rule7))]
("Charlie" "is" "round" "+")
((((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is not smart.
Unknown
inv-rconc
[@1: Dave is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "smart" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "smart" "+")
Dave is not blue.
Unknown
inv-rconc
[@2: Dave is blue.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "blue" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule8 <- rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Harry is not nice.
Unknown
inv-random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is not furry.[(triple1)] Charlie is rough.[(triple2)] Dave is furry.[(triple3)] Dave is nice.[(triple4)] Dave is rough.[(triple5 OR ((triple3) -> rule5))] Harry is blue.[(triple6)] Harry is rough.[(triple7)] @1: Charlie is smart.[(((triple2 triple1) -> rule2))] @2: Charlie is blue.[(((((triple2 triple1) -> rule2)) -> rule1))] @3: Charlie is not round.[(((((((triple2 triple1) -> rule2)) -> rule1) ((triple2 triple1) -> rule2)) -> rule7))]
Charlie is not furry.
("Charlie" "is" "furry" "-")
triple1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple2
Dave is furry.
("Dave" "is" "furry" "+")
triple3
Dave is nice.
("Dave" "is" "nice" "+")
triple4
Dave is rough.
("Dave" "is" "rough" "+")
triple5
((triple3) -> (rule5 % int1))
Dave is rough.
("Dave" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
triple6
Harry is rough.
("Harry" "is" "rough" "+")
triple7
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2 triple1) -> (rule2 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple2 triple1) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not round.
("Charlie" "is" "round" "-")
((((((triple2 triple1) -> (rule2 % int3))) -> (rule1 % int2)) ((triple2 triple1) -> (rule2 % int3))) -> (rule7 % int1))
Charlie is not round.
("Charlie" "is" "round" "-")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3