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