Bob is nice. Charlie is cold. Dave is smart. Harry is quiet. If Harry is cold then Harry is green. All quiet people are smart. If Harry is smart then Harry is cold. All nice people are round. If someone is round and nice then they are quiet. All green, smart people are round. Green people are furry. All smart, green people are round.
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If Harry is cold then Harry is green.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "green" "+"))
All quiet people are smart.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "smart" "+"))
If Harry is smart then Harry is cold.
((("Harry" "is" "smart" "+")) -> ("Harry" "is" "cold" "+"))
All nice people are round.
((("someone" "is" "nice" "+")) -> ("someone" "is" "round" "+"))
If someone is round and nice then they are quiet.
((("someone" "is" "round" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "quiet" "+"))
All green, smart people are round.
((("someone" "is" "green" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "round" "+"))
Green people are furry.
((("someone" "is" "green" "+")) -> ("someone" "is" "furry" "+"))
All smart, green people are round.
((("someone" "is" "smart" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "round" "+"))
Bob is nice.
True
1
proof
[(triple1)]
("Bob" "is" "nice" "+")
triple1
Charlie is not cold.
False
1
inv-proof
[(triple2)]
("Charlie" "is" "cold" "-")
triple2
Bob is round.
True
2
proof
[(((triple1) -> rule4))]
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is not smart.
False
2
inv-proof
[(((triple4) -> rule2))]
("Harry" "is" "smart" "-")
((triple4) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is quiet.
True
4
proof
[(((((triple1) -> rule4) triple1) -> rule5))]
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is not cold.
False
3
inv-proof
[(((((triple4) -> rule2)) -> rule3))]
("Harry" "is" "cold" "-")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Dave is not furry.
Unknown
inv-rconc
[@1: Dave is furry.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Dave" "is" "furry" "-")
Dave is round.
Unknown
rconc
[@1: Dave is round.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Dave" "is" "round" "+")
Charlie is not quiet.
Unknown
inv-rconc
[@1: Charlie is quiet.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "quiet" "-")
Harry is nice.
Unknown
random
[@0: Harry is nice.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "nice" "+")
Dave is not nice.
Unknown
inv-random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
@0: Bob is nice.[(triple1)] Charlie is cold.[(triple2)] Dave is smart.[(triple3)] Harry is quiet.[(triple4)] @1: Bob is round.[(((triple1) -> rule4))] Harry is smart.[(((triple4) -> rule2))] @2: Bob is quiet.[(((((triple1) -> rule4) triple1) -> rule5))] Harry is cold.[(((((triple4) -> rule2)) -> rule3))] @3: Bob is smart.[(((((((triple1) -> rule4) triple1) -> rule5)) -> rule2))] Harry is green.[(((((((triple4) -> rule2)) -> rule3)) -> rule1))] @4: Harry is furry.[(((((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule7))] Harry is round.[(((((triple4) -> rule2) ((((((triple4) -> rule2)) -> rule3)) -> rule1)) -> rule8) OR ((((((((triple4) -> rule2)) -> rule3)) -> rule1) ((triple4) -> rule2)) -> rule6))]
Bob is nice.
("Bob" "is" "nice" "+")
triple1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple4
Bob is round.
("Bob" "is" "round" "+")
((triple1) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
((((triple1) -> (rule4 % int2)) triple1) -> (rule5 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is round.
("Bob" "is" "round" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((triple4) -> (rule2 % int2))) -> (rule3 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((((triple1) -> (rule4 % int3)) triple1) -> (rule5 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((triple4) -> (rule2 % int3))) -> (rule3 % int2))) -> (rule1 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
((((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is round.
("Harry" "is" "round" "+")
((((triple4) -> (rule2 % int4)) ((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule8 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
((((((((triple4) -> (rule2 % int4))) -> (rule3 % int3))) -> (rule1 % int2)) ((triple4) -> (rule2 % int4))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4