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