Bob is big. Bob is green. Bob is nice. Bob is smart. Charlie is big. Charlie is green. Charlie is smart. Erin is furry. Erin is green. Harry is big. Harry is furry. Harry is green. Harry is nice. Harry is smart. Harry is white. If something is white and cold then it is nice. White, nice things are green. If something is smart then it is white. White, big things are green. If Charlie is white then Charlie is nice. If Harry is white and Harry is smart then Harry is furry. If something is nice then it is furry. If something is smart then it is green.
Bob is big.
("Bob" "is" "big" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is smart.
("Bob" "is" "smart" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Erin is green.
("Erin" "is" "green" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is furry.
("Harry" "is" "furry" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is white.
("Harry" "is" "white" "+")
If something is white and cold then it is nice.
((("something" "is" "white" "+") ("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
White, nice things are green.
((("something" "is" "white" "+") ("something" "is" "nice" "+")) -> ("something" "is" "green" "+"))
If something is smart then it is white.
((("something" "is" "smart" "+")) -> ("something" "is" "white" "+"))
White, big things are green.
((("something" "is" "white" "+") ("something" "is" "big" "+")) -> ("something" "is" "green" "+"))
If Charlie is white then Charlie is nice.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "nice" "+"))
If Harry is white and Harry is smart then Harry is furry.
((("Harry" "is" "white" "+") ("Harry" "is" "smart" "+")) -> ("Harry" "is" "furry" "+"))
If something is nice then it is furry.
((("something" "is" "nice" "+")) -> ("something" "is" "furry" "+"))
If something is smart then it is green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "+"))
Charlie is smart.
True
1
proof
[(triple7)]
("Charlie" "is" "smart" "+")
triple7
Bob is not big.
False
1
inv-proof
[(triple1)]
("Bob" "is" "big" "-")
triple1
Bob is furry.
True
2
proof
[(((triple3) -> rule7))]
("Bob" "is" "furry" "+")
((triple3) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Charlie is not white.
False
2
inv-proof
[(((triple7) -> rule3))]
("Charlie" "is" "white" "-")
((triple7) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
True
3
proof
[(((((triple7) -> rule3)) -> rule5))]
("Charlie" "is" "nice" "+")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is not nice.
False
3
inv-proof
[(((((triple7) -> rule3)) -> rule5))]
("Charlie" "is" "nice" "-")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
True
4
proof
[(((((((triple7) -> rule3)) -> rule5)) -> rule7))]
("Charlie" "is" "furry" "+")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is not furry.
False
4
inv-proof
[(((((((triple7) -> rule3)) -> rule5)) -> rule7))]
("Charlie" "is" "furry" "-")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Erin is not white.
Unknown
inv-rconc
[@1: Erin is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "white" "-")
Erin is nice.
Unknown
rconc
[@1: Erin is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "nice" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Erin is smart.
Unknown
random
[@0: Erin is smart.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "smart" "+")
Harry is not cold.
Unknown
inv-random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "-")
Erin is big.
Unknown
random
[@0: Erin is big.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "big" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is big.[(triple1)] Bob is green.[(triple2 OR ((triple4) -> rule8) OR ((((triple4) -> rule3) triple1) -> rule4) OR ((((triple4) -> rule3) triple3) -> rule2))] Bob is nice.[(triple3)] Bob is smart.[(triple4)] Charlie is big.[(triple5)] Charlie is green.[(triple6 OR ((triple7) -> rule8) OR ((((triple7) -> rule3) triple5) -> rule4) OR ((((triple7) -> rule3) ((((triple7) -> rule3)) -> rule5)) -> rule2))] Charlie is smart.[(triple7)] Erin is furry.[(triple8)] Erin is green.[(triple9)] Harry is big.[(triple10)] Harry is furry.[(triple11 OR ((triple13) -> rule7) OR ((triple15 triple14) -> rule6) OR ((((triple14) -> rule3) triple14) -> rule6))] Harry is green.[(triple12 OR ((triple14) -> rule8) OR ((triple15 triple10) -> rule4) OR ((triple15 triple13) -> rule2) OR ((((triple14) -> rule3) triple10) -> rule4) OR ((((triple14) -> rule3) triple13) -> rule2))] Harry is nice.[(triple13)] Harry is smart.[(triple14)] Harry is white.[(triple15 OR ((triple14) -> rule3))] @1: Bob is furry.[(((triple3) -> rule7))] Bob is white.[(((triple4) -> rule3))] Charlie is white.[(((triple7) -> rule3))] @2: Charlie is nice.[(((((triple7) -> rule3)) -> rule5))] @3: Charlie is furry.[(((((((triple7) -> rule3)) -> rule5)) -> rule7))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is green.
("Bob" "is" "green" "+")
triple2
((triple4) -> (rule8 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple4) -> (rule3 % int2)) triple1) -> (rule4 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((triple4) -> (rule3 % int2)) triple3) -> (rule2 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple3
Bob is smart.
("Bob" "is" "smart" "+")
triple4
Charlie is big.
("Charlie" "is" "big" "+")
triple5
Charlie is green.
("Charlie" "is" "green" "+")
triple6
((triple7) -> (rule8 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((triple7) -> (rule3 % int2)) triple5) -> (rule4 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
((((triple7) -> (rule3 % int3)) ((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule2 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple7
Erin is furry.
("Erin" "is" "furry" "+")
triple8
Erin is green.
("Erin" "is" "green" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
Harry is furry.
("Harry" "is" "furry" "+")
triple11
((triple13) -> (rule7 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((triple15 triple14) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
((((triple14) -> (rule3 % int2)) triple14) -> (rule6 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
triple12
((triple14) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple15 triple10) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple15 triple13) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((((triple14) -> (rule3 % int2)) triple10) -> (rule4 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((triple14) -> (rule3 % int2)) triple13) -> (rule2 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is nice.
("Harry" "is" "nice" "+")
triple13
Harry is smart.
("Harry" "is" "smart" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
((triple14) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Bob is furry.
("Bob" "is" "furry" "+")
((triple3) -> (rule7 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple4) -> (rule3 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
((triple7) -> (rule3 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
((((triple7) -> (rule3 % int2))) -> (rule5 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Charlie is white.
("Charlie" "is" "white" "+")
int2
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((triple7) -> (rule3 % int3))) -> (rule5 % int2))) -> (rule7 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is white.
("Charlie" "is" "white" "+")
int3