Bob is furry. Bob is rough. Fiona is cold. Fiona is furry. Fiona is rough. Fiona is smart. Harry is not cold. Harry is quiet. Harry is rough. Harry is white. Quiet, big people are smart. Big, furry people are not cold. If someone is white then they are big. White, quiet people are big. Furry, rough people are not quiet. If Bob is rough then Bob is white.
Bob is furry.
("Bob" "is" "furry" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is not cold.
("Harry" "is" "cold" "-")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Quiet, big people are smart.
((("someone" "is" "quiet" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "smart" "+"))
Big, furry people are not cold.
((("someone" "is" "big" "+") ("someone" "is" "furry" "+")) -> ("someone" "is" "cold" "-"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
White, quiet people are big.
((("someone" "is" "white" "+") ("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Furry, rough people are not quiet.
((("someone" "is" "furry" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "quiet" "-"))
If Bob is rough then Bob is white.
((("Bob" "is" "rough" "+")) -> ("Bob" "is" "white" "+"))
Fiona is smart.
True
1
proof
[(triple6)]
("Fiona" "is" "smart" "+")
triple6
Fiona is not cold.
False
1
inv-proof
[(triple3)]
("Fiona" "is" "cold" "-")
triple3
Bob is not quiet.
True
3
proof
[(((triple1 triple2) -> rule5))]
("Bob" "is" "quiet" "-")
((triple1 triple2) -> (rule5 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Harry is not big.
False
2
inv-proof
[(((triple10) -> rule3) OR ((triple10 triple8) -> rule4))]
("Harry" "is" "big" "-")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 triple8) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is smart.
True
4
proof
[(((triple8 ((triple10) -> rule3)) -> rule1) OR ((triple8 ((triple10 triple8) -> rule4)) -> rule1))]
("Harry" "is" "smart" "+")
((triple8 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple8 ((triple10 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple2) -> rule6)) -> rule3))]
("Bob" "is" "big" "-")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is not cold.
True
5
proof
[(((((((triple2) -> rule6)) -> rule3) triple1) -> rule2))]
("Bob" "is" "cold" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is cold.
False
5
inv-proof
[(((((((triple2) -> rule6)) -> rule3) triple1) -> rule2))]
("Bob" "is" "cold" "+")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Fiona is big.
Unknown
rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
@0: Bob is furry.[(triple1)] Bob is rough.[(triple2)] Fiona is cold.[(triple3)] Fiona is furry.[(triple4)] Fiona is rough.[(triple5)] Fiona is smart.[(triple6)] Harry is not cold.[(triple7)] Harry is quiet.[(triple8)] Harry is rough.[(triple9)] Harry is white.[(triple10)] @1: Bob is not quiet.[(((triple1 triple2) -> rule5))] Bob is white.[(((triple2) -> rule6))] Fiona is not quiet.[(((triple4 triple5) -> rule5))] Harry is big.[(((triple10) -> rule3) OR ((triple10 triple8) -> rule4))] @2: Bob is big.[(((((triple2) -> rule6)) -> rule3))] Harry is smart.[(((triple8 ((triple10) -> rule3)) -> rule1) OR ((triple8 ((triple10 triple8) -> rule4)) -> rule1))] @3: Bob is not cold.[(((((((triple2) -> rule6)) -> rule3) triple1) -> rule2))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Bob is rough.
("Bob" "is" "rough" "+")
triple2
Fiona is cold.
("Fiona" "is" "cold" "+")
triple3
Fiona is furry.
("Fiona" "is" "furry" "+")
triple4
Fiona is rough.
("Fiona" "is" "rough" "+")
triple5
Fiona is smart.
("Fiona" "is" "smart" "+")
triple6
Harry is not cold.
("Harry" "is" "cold" "-")
triple7
Harry is quiet.
("Harry" "is" "quiet" "+")
triple8
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is white.
("Harry" "is" "white" "+")
triple10
Bob is not quiet.
("Bob" "is" "quiet" "-")
((triple1 triple2) -> (rule5 % int1))
Bob is not quiet.
("Bob" "is" "quiet" "-")
int1
Bob is white.
("Bob" "is" "white" "+")
((triple2) -> (rule6 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
((triple4 triple5) -> (rule5 % int1))
Fiona is not quiet.
("Fiona" "is" "quiet" "-")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple10) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((triple10 triple8) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple2) -> (rule6 % int2))) -> (rule3 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
((triple8 ((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((triple8 ((triple10 triple8) -> (rule4 % int2))) -> (rule1 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not cold.
("Bob" "is" "cold" "-")
((((((triple2) -> (rule6 % int3))) -> (rule3 % int2)) triple1) -> (rule2 % int1))
Bob is not cold.
("Bob" "is" "cold" "-")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3