Bob is cold. Bob is furry. Bob is nice. Bob is white. Fiona is cold. Fiona is not furry. Fiona is quiet. Fiona is not round. Gary is round. Harry is furry. Harry is quiet. Harry is not smart. All round, smart things are nice. If something is quiet and smart then it is not nice. All cold, furry things are nice. If something is white then it is furry. Nice things are white. Round things are smart. If Gary is white then Gary is smart. Nice, furry things are cold.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is not furry.
("Fiona" "is" "furry" "-")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is not round.
("Fiona" "is" "round" "-")
Gary is round.
("Gary" "is" "round" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
All round, smart things are nice.
((("something" "is" "round" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and smart then it is not nice.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "nice" "-"))
All cold, furry things are nice.
((("something" "is" "cold" "+") ("something" "is" "furry" "+")) -> ("something" "is" "nice" "+"))
If something is white then it is furry.
((("something" "is" "white" "+")) -> ("something" "is" "furry" "+"))
Nice things are white.
((("something" "is" "nice" "+")) -> ("something" "is" "white" "+"))
Round things are smart.
((("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
If Gary is white then Gary is smart.
((("Gary" "is" "white" "+")) -> ("Gary" "is" "smart" "+"))
Nice, furry things are cold.
((("something" "is" "nice" "+") ("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Bob is white.
True
1
proof
[(triple4 OR ((triple3) -> rule5) OR ((((triple1 triple2) -> rule3)) -> rule5))]
("Bob" "is" "white" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not cold.
False
1
inv-proof
[(triple1 OR ((triple3 triple2) -> rule8) OR ((triple3 ((triple4) -> rule4)) -> rule8) OR ((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule8))]
("Bob" "is" "cold" "-")
triple1
((triple3 triple2) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Gary is smart.
True
2
proof
[(((triple9) -> rule6))]
("Gary" "is" "smart" "+")
((triple9) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is not smart.
False
2
inv-proof
[(((triple9) -> rule6))]
("Gary" "is" "smart" "-")
((triple9) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
True
4
proof
[(((triple9 ((triple9) -> rule6)) -> rule1))]
("Gary" "is" "nice" "+")
((triple9 ((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is not nice.
False
4
inv-proof
[(((triple9 ((triple9) -> rule6)) -> rule1))]
("Gary" "is" "nice" "-")
((triple9 ((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
True
5
proof
[(((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5))]
("Gary" "is" "white" "+")
((((triple9 ((triple9) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not white.
False
5
inv-proof
[(((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5))]
("Gary" "is" "white" "-")
((((triple9 ((triple9) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is furry.
True
6
proof
[(((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "furry" "+")
((((((triple9 ((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is not furry.
False
6
inv-proof
[(((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4))]
("Gary" "is" "furry" "-")
((((((triple9 ((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
True
11
proof
[(((((triple9 ((triple9) -> rule6)) -> rule1) ((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
("Gary" "is" "cold" "+")
((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4)) ((((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Gary is not cold.
False
11
inv-proof
[(((((triple9 ((triple9) -> rule6)) -> rule1) ((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
("Gary" "is" "cold" "-")
((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4)) ((((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5
Harry is not white.
Unknown
inv-rconc
[@4: Harry is white.[CWA. Example of deepest failure = (rule5 <- rule3 <- rule8 <- rule1 <- FAIL)]]
("Harry" "is" "white" "-")
Fiona is nice.
Unknown
rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "nice" "+")
Harry is not cold.
Unknown
inv-rconc
[@2: Harry is cold.[CWA. Example of deepest failure = (rule8 <- rule1 <- FAIL)]]
("Harry" "is" "cold" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
Fiona is not white.
Unknown
inv-rconc
[@2: Fiona is white.[CWA. Example of deepest failure = (rule5 <- rule1 <- FAIL)]]
("Fiona" "is" "white" "-")
Harry is nice.
Unknown
rconc
[@3: Harry is nice.[CWA. Example of deepest failure = (rule3 <- rule8 <- rule1 <- FAIL)]]
("Harry" "is" "nice" "+")
Gary is not quiet.
Unknown
inv-random
[@0: Gary is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "quiet" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
Bob is not round.
Unknown
inv-random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "-")
Bob is quiet.
Unknown
random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "+")
@0: Bob is cold.[(triple1 OR ((triple3 triple2) -> rule8) OR ((triple3 ((triple4) -> rule4)) -> rule8) OR ((triple3 ((((triple3) -> rule5)) -> rule4)) -> rule8))] Bob is furry.[(triple2 OR ((triple4) -> rule4) OR ((((triple3) -> rule5)) -> rule4))] Bob is nice.[(triple3 OR ((triple1 triple2) -> rule3) OR ((triple1 ((triple4) -> rule4)) -> rule3))] Bob is white.[(triple4 OR ((triple3) -> rule5) OR ((((triple1 triple2) -> rule3)) -> rule5))] Fiona is cold.[(triple5)] Fiona is not furry.[(triple6)] Fiona is not round.[(triple8)] Fiona is quiet.[(triple7)] Gary is round.[(triple9)] Harry is furry.[(triple10)] Harry is not smart.[(triple12)] Harry is quiet.[(triple11)] @1: Gary is smart.[(((triple9) -> rule6))] @2: Gary is nice.[(((triple9 ((triple9) -> rule6)) -> rule1))] @3: Gary is white.[(((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5))] @4: Gary is furry.[(((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4))] @5: Gary is cold.[(((((triple9 ((triple9) -> rule6)) -> rule1) ((((((triple9 ((triple9) -> rule6)) -> rule1)) -> rule5)) -> rule4)) -> rule8))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
((triple3 triple2) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
((triple3 ((triple4) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
((triple3 ((((triple3) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is furry.
("Bob" "is" "furry" "+")
triple2
((triple4) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
((((triple3) -> (rule5 % int2))) -> (rule4 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
((triple1 triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((triple1 ((triple4) -> (rule4 % int2))) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
triple4
((triple3) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple1 triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple5
Fiona is not furry.
("Fiona" "is" "furry" "-")
triple6
Fiona is not round.
("Fiona" "is" "round" "-")
triple8
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple7
Gary is round.
("Gary" "is" "round" "+")
triple9
Harry is furry.
("Harry" "is" "furry" "+")
triple10
Harry is not smart.
("Harry" "is" "smart" "-")
triple12
Harry is quiet.
("Harry" "is" "quiet" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
((triple9) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
((triple9 ((triple9) -> (rule6 % int2))) -> (rule1 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
((((triple9 ((triple9) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule5 % int1))
Gary is white.
("Gary" "is" "white" "+")
int1
Gary is nice.
("Gary" "is" "nice" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is furry.
("Gary" "is" "furry" "+")
((((((triple9 ((triple9) -> (rule6 % int4))) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Gary is furry.
("Gary" "is" "furry" "+")
int1
Gary is white.
("Gary" "is" "white" "+")
int2
Gary is nice.
("Gary" "is" "nice" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is cold.
("Gary" "is" "cold" "+")
((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4)) ((((((triple9 ((triple9) -> (rule6 % int5))) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule8 % int1))
Gary is cold.
("Gary" "is" "cold" "+")
int1
Gary is furry.
("Gary" "is" "furry" "+")
int2
Gary is white.
("Gary" "is" "white" "+")
int3
Gary is nice.
("Gary" "is" "nice" "+")
int4
Gary is smart.
("Gary" "is" "smart" "+")
int5