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