Bob is cold. Bob is not nice. Erin is cold. Erin is not furry. Erin is nice. Erin is not rough. Erin is smart. Gary is green. Gary is kind. Harry is not green. Harry is rough. If someone is rough then they are smart. Rough, smart people are furry. If someone is smart and not rough then they are green. If Gary is kind then Gary is not smart. If Harry is cold and Harry is smart then Harry is kind. If someone is cold and not green then they are nice. If someone is furry and smart then they are nice. If Harry is cold then Harry is furry. If Harry is nice then Harry is cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is not furry.
("Erin" "is" "furry" "-")
Erin is nice.
("Erin" "is" "nice" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is smart.
("Erin" "is" "smart" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Harry is not green.
("Harry" "is" "green" "-")
Harry is rough.
("Harry" "is" "rough" "+")
If someone is rough then they are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
Rough, smart people are furry.
((("someone" "is" "rough" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
If someone is smart and not rough then they are green.
((("someone" "is" "smart" "+") ("someone" "is" "rough" "~")) -> ("someone" "is" "green" "+"))
If Gary is kind then Gary is not smart.
((("Gary" "is" "kind" "+")) -> ("Gary" "is" "smart" "-"))
If Harry is cold and Harry is smart then Harry is kind.
((("Harry" "is" "cold" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "kind" "+"))
If someone is cold and not green then they are nice.
((("someone" "is" "cold" "+") ("someone" "is" "green" "~")) -> ("someone" "is" "nice" "+"))
If someone is furry and smart then they are nice.
((("someone" "is" "furry" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "nice" "+"))
If Harry is cold then Harry is furry.
((("Harry" "is" "cold" "+")) -> ("Harry" "is" "furry" "+"))
If Harry is nice then Harry is cold.
((("Harry" "is" "nice" "+")) -> ("Harry" "is" "cold" "+"))
Gary is green.
True
1
proof
[(triple8)]
("Gary" "is" "green" "+")
triple8
Erin is not nice.
False
1
inv-proof
[(triple5)]
("Erin" "is" "nice" "-")
triple5
Erin is green.
True
3
proof
[(((triple7 triple6) -> rule3))]
("Erin" "is" "green" "+")
((triple7 triple6) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Erin is not green.
False
3
inv-proof
[(((triple7 triple6) -> rule3))]
("Erin" "is" "green" "-")
((triple7 triple6) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Harry is furry.
True
4
proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "furry" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is not furry.
False
4
inv-proof
[(((triple11 ((triple11) -> rule1)) -> rule2))]
("Harry" "is" "furry" "-")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
True
7
proof
[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7))]
("Harry" "is" "nice" "+")
((((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2)) ((triple11) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is not nice.
False
7
inv-proof
[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7))]
("Harry" "is" "nice" "-")
((((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2)) ((triple11) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is cold.
True
8
proof
[(((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9))]
("Harry" "is" "cold" "+")
((((((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3)) ((triple11) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is not cold.
False
8
inv-proof
[(((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9))]
("Harry" "is" "cold" "-")
((((((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3)) ((triple11) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is kind.
True
11
proof
[(((((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9) ((triple11) -> rule1)) -> rule5))]
("Harry" "is" "kind" "+")
((((((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple11) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule9 % int2)) ((triple11) -> (rule1 % int5))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5
Harry is not kind.
False
11
inv-proof
[(((((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9) ((triple11) -> rule1)) -> rule5))]
("Harry" "is" "kind" "-")
((((((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple11) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule9 % int2)) ((triple11) -> (rule1 % int5))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5
Bob is not furry.
Unknown
inv-rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Bob" "is" "furry" "-")
Gary is nice.
Unknown
rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Gary" "is" "nice" "+")
Gary is not furry.
Unknown
inv-rconc
[@1: Gary is furry.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "furry" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "+")
Bob is not green.
Unknown
inv-rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "green" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
Gary is not rough.
Unknown
inv-random
[@0: Gary is rough.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "rough" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
Bob is not kind.
Unknown
inv-random
[@0: Bob is kind.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "kind" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Bob is cold.[(triple1)] Bob is not nice.[(triple2)] Erin is cold.[(triple3)] Erin is nice.[(triple5)] Erin is not furry.[(triple4)] Erin is not rough.[(triple6)] Erin is smart.[(triple7)] Gary is green.[(triple8)] Gary is kind.[(triple9)] Harry is not green.[(triple10)] Harry is rough.[(triple11)] @1: Erin is green.[(((triple7 triple6) -> rule3))] Gary is not smart.[(((triple9) -> rule4))] Harry is smart.[(((triple11) -> rule1))] @2: Harry is furry.[(((triple11 ((triple11) -> rule1)) -> rule2))] @3: Harry is nice.[(((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7))] @4: Harry is cold.[(((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9))] @5: Harry is kind.[(((((((((triple11 ((triple11) -> rule1)) -> rule2) ((triple11) -> rule1)) -> rule7)) -> rule9) ((triple11) -> rule1)) -> rule5))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is not nice.
("Bob" "is" "nice" "-")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
Erin is nice.
("Erin" "is" "nice" "+")
triple5
Erin is not furry.
("Erin" "is" "furry" "-")
triple4
Erin is not rough.
("Erin" "is" "rough" "-")
triple6
Erin is smart.
("Erin" "is" "smart" "+")
triple7
Gary is green.
("Gary" "is" "green" "+")
triple8
Gary is kind.
("Gary" "is" "kind" "+")
triple9
Harry is not green.
("Harry" "is" "green" "-")
triple10
Harry is rough.
("Harry" "is" "rough" "+")
triple11
Erin is green.
("Erin" "is" "green" "+")
((triple7 triple6) -> (rule3 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Gary is not smart.
("Gary" "is" "smart" "-")
((triple9) -> (rule4 % int1))
Gary is not smart.
("Gary" "is" "smart" "-")
int1
Harry is smart.
("Harry" "is" "smart" "+")
((triple11) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
((triple11 ((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
((((triple11 ((triple11) -> (rule1 % int3))) -> (rule2 % int2)) ((triple11) -> (rule1 % int3))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is furry.
("Harry" "is" "furry" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
int3
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple11 ((triple11) -> (rule1 % int4))) -> (rule2 % int3)) ((triple11) -> (rule1 % int4))) -> (rule7 % int2))) -> (rule9 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
int3
Harry is smart.
("Harry" "is" "smart" "+")
int4
Harry is kind.
("Harry" "is" "kind" "+")
((((((((triple11 ((triple11) -> (rule1 % int5))) -> (rule2 % int4)) ((triple11) -> (rule1 % int5))) -> (rule7 % int3))) -> (rule9 % int2)) ((triple11) -> (rule1 % int5))) -> (rule5 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
int3
Harry is furry.
("Harry" "is" "furry" "+")
int4
Harry is smart.
("Harry" "is" "smart" "+")
int5