Bob is big. Charlie is young. Gary is not rough. Harry is big. If someone is nice and furry then they are smart. All nice people are smart. If Charlie is big and Charlie is rough then Charlie is furry. If Bob is round then Bob is smart. If someone is smart and furry then they are young. Round, smart people are young. Young people are big. Big people are rough.
Bob is big.
("Bob" "is" "big" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Gary is not rough.
("Gary" "is" "rough" "-")
Harry is big.
("Harry" "is" "big" "+")
If someone is nice and furry then they are smart.
((("someone" "is" "nice" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "smart" "+"))
All nice people are smart.
((("someone" "is" "nice" "+")) -> ("someone" "is" "smart" "+"))
If Charlie is big and Charlie is rough then Charlie is furry.
((("Charlie" "is" "big" "+") ("Charlie" "is" "rough" "+")) -> ("Charlie" "is" "furry" "+"))
If Bob is round then Bob is smart.
((("Bob" "is" "round" "+")) -> ("Bob" "is" "smart" "+"))
If someone is smart and furry then they are young.
((("someone" "is" "smart" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "young" "+"))
Round, smart people are young.
((("someone" "is" "round" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Young people are big.
((("someone" "is" "young" "+")) -> ("someone" "is" "big" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple4)]
("Harry" "is" "big" "-")
triple4
Harry is rough.
True
2
proof
[(((triple4) -> rule8))]
("Harry" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is not big.
False
2
inv-proof
[(((triple2) -> rule7))]
("Charlie" "is" "big" "-")
((triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is rough.
True
3
proof
[(((((triple2) -> rule7)) -> rule8))]
("Charlie" "is" "rough" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not rough.
False
3
inv-proof
[(((((triple2) -> rule7)) -> rule8))]
("Charlie" "is" "rough" "-")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "smart" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Gary" "is" "smart" "+")
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "young" "-")
Charlie is nice.
Unknown
random
[@0: Charlie is nice.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "nice" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Bob is big.[(triple1)] Charlie is young.[(triple2)] Gary is not rough.[(triple3)] Harry is big.[(triple4)] @1: Bob is rough.[(((triple1) -> rule8))] Charlie is big.[(((triple2) -> rule7))] Harry is rough.[(((triple4) -> rule8))] @2: Charlie is rough.[(((((triple2) -> rule7)) -> rule8))] @3: Charlie is furry.[(((((triple2) -> rule7) ((((triple2) -> rule7)) -> rule8)) -> rule3))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Charlie is young.
("Charlie" "is" "young" "+")
triple2
Gary is not rough.
("Gary" "is" "rough" "-")
triple3
Harry is big.
("Harry" "is" "big" "+")
triple4
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule8 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule7 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple4) -> (rule8 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
((((triple2) -> (rule7 % int2))) -> (rule8 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((triple2) -> (rule7 % int3)) ((((triple2) -> (rule7 % int3))) -> (rule8 % int2))) -> (rule3 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3