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