Bob is furry. Dave is big. Erin is kind. Harry is green. If someone is big and blue then they are rough. If Harry is green and Harry is furry then Harry is cold. All rough people are big. All furry, big people are kind. If someone is furry then they are big. If someone is furry and kind then they are green. All green people are big. All kind, rough people are big.
Bob is furry.
("Bob" "is" "furry" "+")
Dave is big.
("Dave" "is" "big" "+")
Erin is kind.
("Erin" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
If someone is big and blue then they are rough.
((("someone" "is" "big" "+") ("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Harry is green and Harry is furry then Harry is cold.
((("Harry" "is" "green" "+") ("Harry" "is" "furry" "+")) -> ("Harry" "is" "cold" "+"))
All rough people are big.
((("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
All furry, big people are kind.
((("someone" "is" "furry" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "kind" "+"))
If someone is furry then they are big.
((("someone" "is" "furry" "+")) -> ("someone" "is" "big" "+"))
If someone is furry and kind then they are green.
((("someone" "is" "furry" "+") ("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All green people are big.
((("someone" "is" "green" "+")) -> ("someone" "is" "big" "+"))
All kind, rough people are big.
((("someone" "is" "kind" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "big" "+"))
Dave is big.
True
1
proof
[(triple2)]
("Dave" "is" "big" "+")
triple2
Dave is not big.
False
1
inv-proof
[(triple2)]
("Dave" "is" "big" "-")
triple2
Bob is big.
True
2
proof
[(((triple1) -> rule5))]
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple4) -> rule7))]
("Harry" "is" "big" "-")
((triple4) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is kind.
True
4
proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("Bob" "is" "kind" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not kind.
False
4
inv-proof
[(((triple1 ((triple1) -> rule5)) -> rule4))]
("Bob" "is" "kind" "-")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
True
6
proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule4)) -> rule6))]
("Bob" "is" "green" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not green.
False
6
inv-proof
[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule4)) -> rule6))]
("Bob" "is" "green" "-")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is kind.
Unknown
rconc
[@1: Harry is kind.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Harry" "is" "kind" "+")
Bob is not rough.
Unknown
inv-rconc
[@1: Bob is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "rough" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Erin" "is" "big" "+")
Bob is not cold.
Unknown
inv-random
[@0: Bob is cold.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "cold" "-")
Erin is furry.
Unknown
random
[@0: Erin is furry.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "furry" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is cold.
Unknown
random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "+")
@0: Bob is furry.[(triple1)] Dave is big.[(triple2)] Erin is kind.[(triple3)] Harry is green.[(triple4)] @1: Bob is big.[(((triple1) -> rule5))] Harry is big.[(((triple4) -> rule7))] @2: Bob is kind.[(((triple1 ((triple1) -> rule5)) -> rule4))] @3: Bob is green.[(((triple1 ((triple1 ((triple1) -> rule5)) -> rule4)) -> rule6))]
Bob is furry.
("Bob" "is" "furry" "+")
triple1
Dave is big.
("Dave" "is" "big" "+")
triple2
Erin is kind.
("Erin" "is" "kind" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
triple4
Bob is big.
("Bob" "is" "big" "+")
((triple1) -> (rule5 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple4) -> (rule7 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
((triple1 ((triple1) -> (rule5 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
((triple1 ((triple1 ((triple1) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3