Bob is cold. Bob is young. Dave is nice. Fiona is nice. Harry is nice. Harry is smart. Harry is young. All smart, young things are cold. All nice things are smart. Quiet, smart things are round. If something is smart then it is nice. If something is quiet and round then it is smart. All smart things are round. Cold things are nice. Young, red things are quiet.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is young.
("Bob" "is" "young" "+")
Dave is nice.
("Dave" "is" "nice" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
All smart, young things are cold.
((("something" "is" "smart" "+") ("something" "is" "young" "+")) -> ("something" "is" "cold" "+"))
All nice things are smart.
((("something" "is" "nice" "+")) -> ("something" "is" "smart" "+"))
Quiet, smart things are round.
((("something" "is" "quiet" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
If something is smart then it is nice.
((("something" "is" "smart" "+")) -> ("something" "is" "nice" "+"))
If something is quiet and round then it is smart.
((("something" "is" "quiet" "+") ("something" "is" "round" "+")) -> ("something" "is" "smart" "+"))
All smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Cold things are nice.
((("something" "is" "cold" "+")) -> ("something" "is" "nice" "+"))
Young, red things are quiet.
((("something" "is" "young" "+") ("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Bob is cold.
True
1
proof
[(triple1)]
("Bob" "is" "cold" "+")
triple1
Bob is not cold.
False
1
inv-proof
[(triple1)]
("Bob" "is" "cold" "-")
triple1
Dave is smart.
True
2
proof
[(((triple3) -> rule2))]
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is not smart.
False
2
inv-proof
[(((triple4) -> rule2))]
("Fiona" "is" "smart" "-")
((triple4) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Bob is smart.
True
3
proof
[(((((triple1) -> rule7)) -> rule2))]
("Bob" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not smart.
False
3
inv-proof
[(((((triple1) -> rule7)) -> rule2))]
("Bob" "is" "smart" "-")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is round.
True
4
proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule6))]
("Bob" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not round.
False
4
inv-proof
[(((((((triple1) -> rule7)) -> rule2)) -> rule6))]
("Bob" "is" "round" "-")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not quiet.
Unknown
inv-rconc
[@1: Bob is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Bob" "is" "quiet" "-")
Dave is quiet.
Unknown
rconc
[@1: Dave is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Dave" "is" "quiet" "+")
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Fiona is quiet.
Unknown
rconc
[@1: Fiona is quiet.[CWA. Example of deepest failure = (rule8 <- FAIL)]]
("Fiona" "is" "quiet" "+")
Dave is not red.
Unknown
inv-random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Fiona is young.
Unknown
random
[@0: Fiona is young.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "young" "+")
@0: Bob is cold.[(triple1)] Bob is young.[(triple2)] Dave is nice.[(triple3)] Fiona is nice.[(triple4)] Harry is nice.[(triple5 OR ((triple6) -> rule4) OR ((((triple6 triple7) -> rule1)) -> rule7))] Harry is smart.[(triple6 OR ((triple5) -> rule2))] Harry is young.[(triple7)] @1: Bob is nice.[(((triple1) -> rule7))] Dave is smart.[(((triple3) -> rule2))] Fiona is smart.[(((triple4) -> rule2))] Harry is cold.[(((triple6 triple7) -> rule1) OR ((((triple5) -> rule2) triple7) -> rule1))] Harry is round.[(((triple6) -> rule6) OR ((((triple5) -> rule2)) -> rule6))] @2: Bob is smart.[(((((triple1) -> rule7)) -> rule2))] Dave is round.[(((((triple3) -> rule2)) -> rule6))] Fiona is round.[(((((triple4) -> rule2)) -> rule6))] @3: Bob is round.[(((((((triple1) -> rule7)) -> rule2)) -> rule6))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is young.
("Bob" "is" "young" "+")
triple2
Dave is nice.
("Dave" "is" "nice" "+")
triple3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple4
Harry is nice.
("Harry" "is" "nice" "+")
triple5
((triple6) -> (rule4 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
((((triple6 triple7) -> (rule1 % int2))) -> (rule7 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple6
((triple5) -> (rule2 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is nice.
("Bob" "is" "nice" "+")
((triple1) -> (rule7 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
((triple3) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
((triple4) -> (rule2 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple6 triple7) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple5) -> (rule2 % int2)) triple7) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
((triple6) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple5) -> (rule2 % int2))) -> (rule6 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Bob is smart.
("Bob" "is" "smart" "+")
((((triple1) -> (rule7 % int2))) -> (rule2 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Dave is round.
("Dave" "is" "round" "+")
((((triple3) -> (rule2 % int2))) -> (rule6 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
((((triple4) -> (rule2 % int2))) -> (rule6 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Bob is round.
("Bob" "is" "round" "+")
((((((triple1) -> (rule7 % int3))) -> (rule2 % int2))) -> (rule6 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3