Charlie is blue. Gary is big. Gary is blue. Gary is kind. Gary is round. Gary is smart. Gary is young. Harry is blue. Harry is round. Harry is young. If Harry is round then Harry is rough. Rough, blue people are round. All young, big people are round. If someone is rough and blue then they are kind. All young people are round. If Gary is young then Gary is smart. If someone is big then they are round. Smart, rough people are young.
Charlie is blue.
("Charlie" "is" "blue" "+")
Gary is big.
("Gary" "is" "big" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is round.
("Gary" "is" "round" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is round then Harry is rough.
((("Harry" "is" "round" "+")) -> ("Harry" "is" "rough" "+"))
Rough, blue people are round.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "round" "+"))
All young, big people are round.
((("someone" "is" "young" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
If someone is rough and blue then they are kind.
((("someone" "is" "rough" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "kind" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If Gary is young then Gary is smart.
((("Gary" "is" "young" "+")) -> ("Gary" "is" "smart" "+"))
If someone is big then they are round.
((("someone" "is" "big" "+")) -> ("someone" "is" "round" "+"))
Smart, rough people are young.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "young" "+"))
Gary is round.
True
1
proof
[(triple5 OR ((triple2) -> rule7) OR ((triple7) -> rule5) OR ((triple7 triple2) -> rule3))]
("Gary" "is" "round" "+")
triple5
((triple2) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7 triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is not smart.
False
1
inv-proof
[(triple6 OR ((triple7) -> rule6))]
("Gary" "is" "smart" "-")
triple6
((triple7) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Harry is rough.
True
2
proof
[(((triple9) -> rule1) OR ((((triple10) -> rule5)) -> rule1))]
("Harry" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not rough.
False
2
inv-proof
[(((triple9) -> rule1) OR ((((triple10) -> rule5)) -> rule1))]
("Harry" "is" "rough" "-")
((triple9) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
True
4
proof
[(((((triple9) -> rule1) triple8) -> rule4) OR ((((((triple10) -> rule5)) -> rule1) triple8) -> rule4))]
("Harry" "is" "kind" "+")
((((triple9) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not kind.
False
4
inv-proof
[(((((triple9) -> rule1) triple8) -> rule4) OR ((((((triple10) -> rule5)) -> rule1) triple8) -> rule4))]
("Harry" "is" "kind" "-")
((((triple9) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Charlie is not round.
Unknown
inv-rconc
[@2: Charlie is round.[CWA. Example of deepest failure = (rule5 <- rule8 <- FAIL)]]
("Charlie" "is" "round" "-")
Charlie is kind.
Unknown
rconc
[@1: Charlie is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Charlie" "is" "kind" "+")
Charlie is not young.
Unknown
inv-rconc
[@1: Charlie is young.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Charlie" "is" "young" "-")
Charlie is smart.
Unknown
random
[@0: Charlie is smart.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "smart" "+")
Harry is not smart.
Unknown
inv-random
[@0: Harry is smart.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "smart" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Charlie is blue.[(triple1)] Gary is big.[(triple2)] Gary is blue.[(triple3)] Gary is kind.[(triple4)] Gary is round.[(triple5 OR ((triple2) -> rule7) OR ((triple7) -> rule5) OR ((triple7 triple2) -> rule3))] Gary is smart.[(triple6 OR ((triple7) -> rule6))] Gary is young.[(triple7)] Harry is blue.[(triple8)] Harry is round.[(triple9 OR ((triple10) -> rule5))] Harry is young.[(triple10)] @1: Harry is rough.[(((triple9) -> rule1) OR ((((triple10) -> rule5)) -> rule1))] @2: Harry is kind.[(((((triple9) -> rule1) triple8) -> rule4) OR ((((((triple10) -> rule5)) -> rule1) triple8) -> rule4))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Gary is big.
("Gary" "is" "big" "+")
triple2
Gary is blue.
("Gary" "is" "blue" "+")
triple3
Gary is kind.
("Gary" "is" "kind" "+")
triple4
Gary is round.
("Gary" "is" "round" "+")
triple5
((triple2) -> (rule7 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7) -> (rule5 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple7 triple2) -> (rule3 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
triple6
((triple7) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple7
Harry is blue.
("Harry" "is" "blue" "+")
triple8
Harry is round.
("Harry" "is" "round" "+")
triple9
((triple10) -> (rule5 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple10) -> (rule5 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
((((triple9) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
((((((triple10) -> (rule5 % int3))) -> (rule1 % int2)) triple8) -> (rule4 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3