Bob is big. Bob is not green. Erin is big. Erin is not rough. Erin is round. Erin is young. Harry is not smart. If Harry is not big then Harry is young. If something is big then it is not smart. If something is rough and not smart then it is blue. If something is blue then it is not green. If something is smart then it is not green. If something is young then it is not green.
Bob is big.
("Bob" "is" "big" "+")
Bob is not green.
("Bob" "is" "green" "-")
Erin is big.
("Erin" "is" "big" "+")
Erin is not rough.
("Erin" "is" "rough" "-")
Erin is round.
("Erin" "is" "round" "+")
Erin is young.
("Erin" "is" "young" "+")
Harry is not smart.
("Harry" "is" "smart" "-")
If Harry is not big then Harry is young.
((("Harry" "is" "big" "~")) -> ("Harry" "is" "young" "+"))
If something is big then it is not smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "-"))
If something is rough and not smart then it is blue.
((("something" "is" "rough" "+") ("something" "is" "smart" "~")) -> ("something" "is" "blue" "+"))
If something is blue then it is not green.
((("something" "is" "blue" "+")) -> ("something" "is" "green" "-"))
If something is smart then it is not green.
((("something" "is" "smart" "+")) -> ("something" "is" "green" "-"))
If something is young then it is not green.
((("something" "is" "young" "+")) -> ("something" "is" "green" "-"))
Bob is big.
True
1
proof
[(triple1)]
("Bob" "is" "big" "+")
triple1
Erin is not round.
False
1
inv-proof
[(triple5)]
("Erin" "is" "round" "-")
triple5
Bob is not smart.
True
2
proof
[(((triple1) -> rule2))]
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Erin is green.
False
2
inv-proof
[(((triple6) -> rule6))]
("Erin" "is" "green" "+")
((triple6) -> (rule6 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Bob is not blue.
Unknown
inv-rconc
[@1: Bob is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "blue" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not rough.
Unknown
inv-random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "-")
Harry is big.
Unknown
random
[@0: Harry is big.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "big" "+")
@0: Bob is big.[(triple1)] Bob is not green.[(triple2)] Erin is big.[(triple3)] Erin is not rough.[(triple4)] Erin is round.[(triple5)] Erin is young.[(triple6)] Harry is not smart.[(triple7)] @1: Bob is not smart.[(((triple1) -> rule2))] Erin is not green.[(((triple6) -> rule6))] Erin is not smart.[(((triple3) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is not green.
("Bob" "is" "green" "-")
triple2
Erin is big.
("Erin" "is" "big" "+")
triple3
Erin is not rough.
("Erin" "is" "rough" "-")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is young.
("Erin" "is" "young" "+")
triple6
Harry is not smart.
("Harry" "is" "smart" "-")
triple7
Bob is not smart.
("Bob" "is" "smart" "-")
((triple1) -> (rule2 % int1))
Bob is not smart.
("Bob" "is" "smart" "-")
int1
Erin is not green.
("Erin" "is" "green" "-")
((triple6) -> (rule6 % int1))
Erin is not green.
("Erin" "is" "green" "-")
int1
Erin is not smart.
("Erin" "is" "smart" "-")
((triple3) -> (rule2 % int1))
Erin is not smart.
("Erin" "is" "smart" "-")
int1