Charlie is blue. Charlie is furry. Charlie is rough. Charlie is round. Dave is blue. Dave is cold. Dave is furry. Dave is round. Dave is smart. Gary is rough. Harry is blue. Harry is cold. Harry is furry. Harry is round. Harry is smart. All rough, kind people are cold. If someone is smart and rough then they are kind. All furry, round people are smart.
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is furry.
("Dave" "is" "furry" "+")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
All rough, kind people are cold.
((("someone" "is" "rough" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "cold" "+"))
If someone is smart and rough then they are kind.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
All furry, round people are smart.
((("someone" "is" "furry" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "smart" "+"))
Gary is rough.
True
1
proof
[(triple10)]
("Gary" "is" "rough" "+")
triple10
Dave is not smart.
False
1
inv-proof
[(triple9 OR ((triple7 triple8) -> rule3))]
("Dave" "is" "smart" "-")
triple9
((triple7 triple8) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Charlie is smart.
True
3
proof
[(((triple2 triple4) -> rule3))]
("Charlie" "is" "smart" "+")
((triple2 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is not smart.
False
3
inv-proof
[(((triple2 triple4) -> rule3))]
("Charlie" "is" "smart" "-")
((triple2 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
True
5
proof
[(((((triple2 triple4) -> rule3) triple3) -> rule2))]
("Charlie" "is" "kind" "+")
((((triple2 triple4) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is not kind.
False
5
inv-proof
[(((((triple2 triple4) -> rule3) triple3) -> rule2))]
("Charlie" "is" "kind" "-")
((((triple2 triple4) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
True
7
proof
[(((triple3 ((((triple2 triple4) -> rule3) triple3) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "+")
((triple3 ((((triple2 triple4) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Charlie is not cold.
False
7
inv-proof
[(((triple3 ((((triple2 triple4) -> rule3) triple3) -> rule2)) -> rule1))]
("Charlie" "is" "cold" "-")
((triple3 ((((triple2 triple4) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3
Dave is not kind.
Unknown
inv-rconc
[@1: Dave is kind.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "kind" "-")
Gary is kind.
Unknown
rconc
[@2: Gary is kind.[CWA. Example of deepest failure = (rule2 <- rule3 <- FAIL)]]
("Gary" "is" "kind" "+")
Gary is not cold.
Unknown
inv-rconc
[@3: Gary is cold.[CWA. Example of deepest failure = (rule1 <- rule2 <- rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Gary is smart.
Unknown
rconc
[@1: Gary is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "smart" "+")
Gary is not blue.
Unknown
inv-random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "-")
Gary is furry.
Unknown
random
[@0: Gary is furry.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "furry" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is blue.[(triple1)] Charlie is furry.[(triple2)] Charlie is rough.[(triple3)] Charlie is round.[(triple4)] Dave is blue.[(triple5)] Dave is cold.[(triple6)] Dave is furry.[(triple7)] Dave is round.[(triple8)] Dave is smart.[(triple9 OR ((triple7 triple8) -> rule3))] Gary is rough.[(triple10)] Harry is blue.[(triple11)] Harry is cold.[(triple12)] Harry is furry.[(triple13)] Harry is round.[(triple14)] Harry is smart.[(triple15 OR ((triple13 triple14) -> rule3))] @1: Charlie is smart.[(((triple2 triple4) -> rule3))] @2: Charlie is kind.[(((((triple2 triple4) -> rule3) triple3) -> rule2))] @3: Charlie is cold.[(((triple3 ((((triple2 triple4) -> rule3) triple3) -> rule2)) -> rule1))]
Charlie is blue.
("Charlie" "is" "blue" "+")
triple1
Charlie is furry.
("Charlie" "is" "furry" "+")
triple2
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Charlie is round.
("Charlie" "is" "round" "+")
triple4
Dave is blue.
("Dave" "is" "blue" "+")
triple5
Dave is cold.
("Dave" "is" "cold" "+")
triple6
Dave is furry.
("Dave" "is" "furry" "+")
triple7
Dave is round.
("Dave" "is" "round" "+")
triple8
Dave is smart.
("Dave" "is" "smart" "+")
triple9
((triple7 triple8) -> (rule3 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Gary is rough.
("Gary" "is" "rough" "+")
triple10
Harry is blue.
("Harry" "is" "blue" "+")
triple11
Harry is cold.
("Harry" "is" "cold" "+")
triple12
Harry is furry.
("Harry" "is" "furry" "+")
triple13
Harry is round.
("Harry" "is" "round" "+")
triple14
Harry is smart.
("Harry" "is" "smart" "+")
triple15
((triple13 triple14) -> (rule3 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
((triple2 triple4) -> (rule3 % int1))
Charlie is smart.
("Charlie" "is" "smart" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
((((triple2 triple4) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is smart.
("Charlie" "is" "smart" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple3 ((((triple2 triple4) -> (rule3 % int3)) triple3) -> (rule2 % int2))) -> (rule1 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is smart.
("Charlie" "is" "smart" "+")
int3